Metamath Proof Explorer


Theorem barbariALT

Description: Alternate proof of barbari , shorter but using more axioms. See comment of dariiALT . (Contributed by David A. Wheeler, 27-Aug-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses barbari.maj
|- A. x ( ph -> ps )
barbari.min
|- A. x ( ch -> ph )
barbari.e
|- E. x ch
Assertion barbariALT
|- E. x ( ch /\ ps )

Proof

Step Hyp Ref Expression
1 barbari.maj
 |-  A. x ( ph -> ps )
2 barbari.min
 |-  A. x ( ch -> ph )
3 barbari.e
 |-  E. x ch
4 1 2 barbara
 |-  A. x ( ch -> ps )
5 4 spi
 |-  ( ch -> ps )
6 5 ancli
 |-  ( ch -> ( ch /\ ps ) )
7 3 6 eximii
 |-  E. x ( ch /\ ps )