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 𝑥 ( 𝜑𝜓 )
barbari.min 𝑥 ( 𝜒𝜑 )
barbari.e 𝑥 𝜒
Assertion barbariALT 𝑥 ( 𝜒𝜓 )

Proof

Step Hyp Ref Expression
1 barbari.maj 𝑥 ( 𝜑𝜓 )
2 barbari.min 𝑥 ( 𝜒𝜑 )
3 barbari.e 𝑥 𝜒
4 1 2 barbara 𝑥 ( 𝜒𝜓 )
5 4 spi ( 𝜒𝜓 )
6 5 ancli ( 𝜒 → ( 𝜒𝜓 ) )
7 3 6 eximii 𝑥 ( 𝜒𝜓 )