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 )