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

Metamath Proof Explorer

Theorem exlimdh

Description: Deduction form of Theorem 19.9 of Margaris p. 89. (Contributed by NM, 28-Jan-1997)

Ref Expression
Hypotheses exlimdh.1 ⊢ φ → ∀ x φ
exlimdh.2 ⊢ χ → ∀ x χ
exlimdh.3 ⊢ φ → ψ → χ
Assertion exlimdh ⊢ φ → ∃ x ψ → χ

Proof

Step Hyp Ref Expression
1 exlimdh.1 ⊢ φ → ∀ x φ
2 exlimdh.2 ⊢ χ → ∀ x χ
3 exlimdh.3 ⊢ φ → ψ → χ
4 1 nf5i ⊢ Ⅎ x φ
5 2 nf5i ⊢ Ⅎ x χ
6 4 5 3 exlimd ⊢ φ → ∃ x ψ → χ