impbii Show Code edit
# a.k.a. biconsi
## Bicondition from two conditionals
##
## (-> ph ps)
## (-> ps ph)
## (<-> ph ps)
##
thm (impbii () (1 (-> ph ps) 2 (-> ps ph)) (<-> ph ps)
1 2 pm3.2i def-bi-2i)
(<-> ph ps)
edit