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 ⊢ ∀ x φ → ψ
barbari.min ⊢ ∀ x χ → φ
barbari.e ⊢ ∃ x χ
Assertion barbariALT ⊢ ∃ x χ ∧ ψ

Proof

Step Hyp Ref Expression
1 barbari.maj ⊢ ∀ x φ → ψ
2 barbari.min ⊢ ∀ x χ → φ
3 barbari.e ⊢ ∃ x χ
4 1 2 barbara ⊢ ∀ x χ → ψ
5 4 spi ⊢ χ → ψ
6 5 ancli ⊢ χ → χ ∧ ψ
7 3 6 eximii ⊢ ∃ x χ ∧ ψ