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

Metamath Proof Explorer

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	⊢ ∀ 𝑥 ( 𝜑 → 𝜓 )
	barbari.min	⊢ ∀ 𝑥 ( 𝜒 → 𝜑 )
	barbari.e	⊢ ∃ 𝑥 𝜒
Assertion	barbariALT	⊢ ∃ 𝑥 ( 𝜒 ∧ 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		barbari.maj	⊢ ∀ 𝑥 ( 𝜑 → 𝜓 )
2		barbari.min	⊢ ∀ 𝑥 ( 𝜒 → 𝜑 )
3		barbari.e	⊢ ∃ 𝑥 𝜒
4	1 2	barbara	⊢ ∀ 𝑥 ( 𝜒 → 𝜓 )
5	4	spi	⊢ ( 𝜒 → 𝜓 )
6	5	ancli	⊢ ( 𝜒 → ( 𝜒 ∧ 𝜓 ) )
7	3 6	eximii	⊢ ∃ 𝑥 ( 𝜒 ∧ 𝜓 )