Theorem barocoALT

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	baroco.maj	|- A. x ( ph -> ps )
	baroco.min	|- E. x ( ch /\ -. ps )
Assertion	barocoALT	|- E. x ( ch /\ -. ph )

Proof

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