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 ⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
exlimdh.2 ⊢ ( 𝜒 → ∀ 𝑥 𝜒 )
exlimdh.3 ⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
Assertion exlimdh ( 𝜑 → ( ∃ 𝑥 𝜓 → 𝜒 ) )

Proof

Step Hyp Ref Expression
1 exlimdh.1 ⊢ ( 𝜑 → ∀ 𝑥 𝜑 )
2 exlimdh.2 ⊢ ( 𝜒 → ∀ 𝑥 𝜒 )
3 exlimdh.3 ⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
4 1 nf5i ⊢ Ⅎ 𝑥 𝜑
5 2 nf5i ⊢ Ⅎ 𝑥 𝜒
6 4 5 3 exlimd ⊢ ( 𝜑 → ( ∃ 𝑥 𝜓 → 𝜒 ) )