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