ancom Show Code edit
## Commute Conjunction
## right('Commute', '∧')
thm (ancom () () (<-> (/\ ph ps) (/\ ps ph)) ph ps pm3.27 ph ps pm3.26 jca ps ph pm3.27 ps ph pm3.26 jca impbii)
(<-> (/\ ph ps) (/\ ps ph))
edit