andd Show Code edit
## Join consequents
thm (andd () (1 (-> ph ps) 2 (-> ph ch)) (-> ph (/\ ps ch))
2 1 ps ch and syl mpd)
(-> ph (/\ ps ch))
edit