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