This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ∀ 𝑥 ( 𝜑 → 𝜓 )
	baroco.min	⊢ ∃ 𝑥 ( 𝜒 ∧ ¬ 𝜓 )
Assertion	barocoALT	⊢ ∃ 𝑥 ( 𝜒 ∧ ¬ 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		baroco.maj	⊢ ∀ 𝑥 ( 𝜑 → 𝜓 )
2		baroco.min	⊢ ∃ 𝑥 ( 𝜒 ∧ ¬ 𝜓 )
3	1	spi	⊢ ( 𝜑 → 𝜓 )
4	3	con3i	⊢ ( ¬ 𝜓 → ¬ 𝜑 )
5	4	anim2i	⊢ ( ( 𝜒 ∧ ¬ 𝜓 ) → ( 𝜒 ∧ ¬ 𝜑 ) )
6	2 5	eximii	⊢ ∃ 𝑥 ( 𝜒 ∧ ¬ 𝜑 )