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

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

Proof

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