preandi Show Code edit
## Join premises
thm (preandi () (1 ph 2 ps) (-. (-> ph (-. ps)))
2 1 ph ps preand ax-mp ax-mp)
(-. (-> ph (-. ps)))
edit