iman Show Code edit
## AND and → Equivalance
## right('Equivalence', '∧')
thm (iman () () (<-> (-> ph ps) (-. (/\ ph (-. ps))))
ps notnot
(<-> ps (-. (-. ps)))
ph imbi2i
(<-> (-> ph ps) (-> ph (-. (-. ps))))
ph (-. ps) df-an
(<-> (/\ ph (-. ps)) (-. (-> ph (-. (-. ps)))))
con2bii
(<-> (-> ph (-. (-. ps))) (-. (/\ ph (-. ps))))
bitri
(<-> (-> ph ps) (-. (/\ ph (-. ps))))
)
edit