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	$⊢ \forall x (φ \to \neg ψ)$
	festino.min	$⊢ \exists x (χ \land ψ)$
Assertion	festinoALT	$⊢ \exists x (χ \land \neg φ)$

Proof

Step	Hyp	Ref	Expression
1		festino.maj	$⊢ \forall x (φ \to \neg ψ)$
2		festino.min	$⊢ \exists x (χ \land ψ)$
3	1	spi	$⊢ φ \to \neg ψ$
4	3	con2i	$⊢ ψ \to \neg φ$
5	4	anim2i	$⊢ (χ \land ψ) \to (χ \land \neg φ)$
6	2 5	eximii	$⊢ \exists x (χ \land \neg φ)$