Metamath Proof Explorer


Theorem festinoALT

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

Proof

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