anddi Show Code edit
# Double distributive law for conjunction.
## Double Distributive Property
thm (anddi () () (<-> (/\ (\/ ph ps) (\/ ch th)) (\/ (\/ (/\ ph ch) (/\ ph th)) (\/ (/\ ps ch) (/\ ps th)))) ph ps (\/ ch th) andir ph ch th andi ps ch th andi orbi12i bitri)
(<-> (/\ (\/ ph ps) (\/ ch th)) (\/ (\/ (/\ ph ch) (/\ ph th)) (\/ (/\ ps ch) (/\ ps th))))
edit