anandi Show Code edit
# Distribution of conjunction over conjunction.
## Distributive Property
thm (anandi () () (<-> (/\ ph (/\ ps ch)) (/\ (/\ ph ps) (/\ ph ch))) ph anidm (/\ ps ch) anbi1i ph ph ps ch an4 bitr3i)
(<-> (/\ ph (/\ ps ch)) (/\ (/\ ph ps) (/\ ph ch)))
edit