impbid Show Code edit
# Deduce an equivalence from two implications.
## Deduce Biconditional from two conditionals
##
## (-> ph (-> [ ps ch ] ))
## (-> ph (-> [ ch ps ] ))
## (-> ph (<-> [ ps ch ] ))
##
thm (impbid () (impbid.1 (-> ph (-> ps ch)) impbid.2 (-> ph (-> ch ps))) (-> ph (<-> ps ch)) impbid.1 impbid.2 jca ps ch dfbi2 sylibr)
(-> ph (<-> ps ch))
edit