orcom Show Code edit
## Commutative Property of OR
##
## (<-> (\/ ph ps) (\/ ps ph))
##
thm (orcom () () (<-> (\/ ph ps) (\/ ps ph))
ph ps df-or
(<-> (\/ ph ps) (-> (-. ph) ps))
ph ps con1b
(<-> (-> (-. ph) ps) (-> (-. ps) ph))
bitri
(<-> (\/ ph ps) (-> (-. ps) ph))
ps ph df-or
(<-> (\/ ps ph) (-> (-. ps) ph))
bicomi
(<-> (-> (-. ps) ph) (\/ ps ph))
bitri
(<-> (\/ ph ps) (\/ ps ph))
)
edit