Metamath Proof Explorer


Theorem daraptiALT

Description: Alternate proof of darapti , 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 darapti.maj
|- A. x ( ph -> ps )
darapti.min
|- A. x ( ph -> ch )
darapti.e
|- E. x ph
Assertion daraptiALT
|- E. x ( ch /\ ps )

Proof

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