bicomi Show Code edit
## Commutative Property
thm (bicomi () (1 (<-> ph ps)) (<-> ps ph)
1 biimpri
(-> ps ph)
1 biimpi
(-> ph ps)
impbii)
(<-> ps ph)
edit