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