iba Show Code edit
# Introduction of antecedent as conjunct. Theorem *4.73 of
# [bib/WhiteheadRussell] p. 121.
## Introduce antecedent as conjunct
thm (iba () () (-> ph (<-> ps (/\ ps ph))) ph ps ancrb pm5.74ri)
(-> ph (<-> ps (/\ ps ph)))
edit