con34b Show Code edit
## Contrapositive
## right('Equivalence', '←')
thm (con34b () () (<-> (-> ph ps) (-> (-. ps) (-. ph)))
ph ps con3
(-> (-> ph ps) (-> (-. ps) (-. ph)))
ps ph ax-3
(-> (-> (-. ps) (-. ph)) (-> ph ps))
impbii)
(<-> (-> ph ps) (-> (-. ps) (-. ph)))
edit