a1d Show Code edit
## First Axiom Deduction
##
## [ ph
## (-> ps [ ph)
##
thm (a1d () (1 (-> ph ps)) (-> ph (-> ch ps))
1 ch a1i com12)
(-> ph (-> ch ps))
edit