pm4.71 Show Code edit
# Implication in terms of biconditional and conjunction. Theorem *4.71 of
# [bib/WhiteheadRussell] p. 120.
## Implication as a biconditional and conjunction
thm (pm4.71 () () (<-> (-> ph ps) (<-> ph (/\ ph ps))) ph ps ancl ph ps pm3.26 impbid1 ph (/\ ph ps) bi1 ph ps pm3.27 syl6 impbii)
(<-> (-> ph ps) (<-> ph (/\ ph ps)))
edit