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