pm3.2 Show Code edit
# Join antecedents with conjunction. Theorem *3.2 of [bib/WhiteheadRussell]
# p. 111.
## Join antecedents with conjunction
thm (pm3.2 () () (-> ph (-> ps (/\ ph ps))) ph ps df-an biimpri expi)
(-> ph (-> ps (/\ ph ps)))
edit