a3d Show Code edit
## Third Axiom Deduction
##
## Same as con4d just a different name.
##
thm (a3d () (1 (-> ph (-> (-. ps) (-. ch)))) (-> ph (-> ch ps))
1 con4d)
(-> ph (-> ch ps))
edit