pm3.4 Show Code edit
# Conjunction implies implication. Theorem *3.4 of [bib/WhiteheadRussell]
# p. 113.
## Conjunction implies implication
thm (pm3.4 () () (-> (/\ ph ps) (-> ph ps)) ph ps pm3.27 ph a1d)
(-> (/\ ph ps) (-> ph ps))
edit