df-and-2i Show Code edit
## Definition of AND Implication
thm (df-and-2i () (1 (-. (-> ph (-. ps)))) (/\ ph ps)
1 ph ps df-and-2 ax-mp)
(/\ ph ps)
edit