andi Show Code edit
# Distributive law for conjunction. Theorem *4.4 of [bib/WhiteheadRussell]
# p. 118.
## Distributive Property
## right('Distribute', 'L') left('Distribute', '-L')
thm (andi () () (<-> (/\ ph (\/ ps ch)) (\/ (/\ ph ps) (/\ ph ch))) (-. ph) (-. ps) (-. ch) ordi ps ch ioran (-. ph) orbi2i ph ps ianor ph ch ianor anbi12i 3bitr4i notbii ph (\/ ps ch) anor (/\ ph ps) (/\ ph ch) oran 3bitr4i)
(<-> (/\ ph (\/ ps ch)) (\/ (/\ ph ps) (/\ ph ch)))
edit