and2i Show Code edit
## Eliminate Conjunct
thm (and2i () (1 (/\ ph ps)) ps
1 ph ps and2 ax-mp)
ps
edit