orddi Show Code edit
# Double distributive law for disjunction.
## Double Distributive Property
thm (orddi () () (<-> (\/ (/\ ph ps) (/\ ch th)) (/\ (/\ (\/ ph ch) (\/ ph th)) (/\ (\/ ps ch) (\/ ps th)))) ph ps (/\ ch th) ordir ph ch th ordi ps ch th ordi anbi12i bitri)
(<-> (\/ (/\ ph ps) (/\ ch th)) (/\ (/\ (\/ ph ch) (\/ ph th)) (/\ (\/ ps ch) (\/ ps th))))
edit