ordir Show Code edit
## Distributive Property
## right('Distribute', 'R') left('Distribute', '-R')
thm (ordir () () (<-> (\/ (/\ ph ps) ch) (/\ (\/ ph ch) (\/ ps ch))) ch ph ps ordi (/\ ph ps) ch orcom ph ch orcom ps ch orcom anbi12i 3bitr4i)
(<-> (\/ (/\ ph ps) ch) (/\ (\/ ph ch) (\/ ps ch)))
edit