mpan2 Show Code edit
## Remove the true part of a conjunction
##
## [ ps ]
## (-> (/\ ph [ ps ] ) ch)
## (-> ph ] ] ch)
##
thm (mpan2 () (mpan2.1 ps mpan2.2 (-> (/\ ph ps) ch)) (-> ph ch) mpan2.1 mpan2.2 ex mpi)
(-> ph ch)
edit