orordi Show Code edit
## Distribution of disjunction over disjunction
thm (orordi () () (<-> (\/ ph (\/ ps ch)) (\/ (\/ ph ps) (\/ ph ch)))
ph oridm
(<-> (\/ ph ph) ph)
(\/ ps ch) orbi1i
(<-> (\/ (\/ ph ph) (\/ ps ch)) (\/ ph (\/ ps ch)))
ph ph ps ch or4
(<-> (\/ (\/ ph ph) (\/ ps ch)) (\/ (\/ ph ps) (\/ ph ch)))
bitr3i
(<-> (\/ ph (\/ ps ch)) (\/ (\/ ph ps) (\/ ph ch)))
)
edit