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

Metamath Proof Explorer

Theorem daraptiALT

Description: Alternate proof of darapti , 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 darapti.maj ⊢ ∀ x φ → ψ
darapti.min ⊢ ∀ x φ → χ
darapti.e ⊢ ∃ x φ
Assertion daraptiALT ⊢ ∃ x χ ∧ ψ

Proof

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