df-and-1d Show Code edit
## Definition of AND Deduction
thm (df-and-1d () (1 (-> ph (/\ ps ch))) (-> ph (-. (-> ps (-. ch))))
1 ps ch df-and-1 syl)
(-> ph (-. (-> ps (-. ch))))
edit