imbi1i Show Code edit
## Equivalence over Implication
##
## (<-> ph ] ] [ ps ] )
## (<-> (-> ph ] ch) ] (-> [ ps ] ch))
##
thm (imbi1i () (1 (<-> ph ps)) (<-> (-> ph ch) (-> ps ch))
1 biimpri ch imim1i
(-> (-> ph ch) (-> ps ch))
1 biimpi ch imim1i
(-> (-> ps ch) (-> ph ch))
impbii)
(<-> (-> ph ch) (-> ps ch))
edit