imbi2i Show Code edit
# Ok, some constructors
## Equivalence over Implication
##
## (<-> [ ph ] [ [ ps)
## (<-> (-> ch [ ph ] ) [ (-> ch [ ps))
##
thm (imbi2i () (1 (<-> ph ps)) (<-> (-> ch ph) (-> ch ps))
1 biimpi ch imim2i
(-> (-> ch ph) (-> ch ps))
1 biimpri ch imim2i
(-> (-> ch ps) (-> ch ph))
impbii)
(<-> (-> ch ph) (-> ch ps))
edit