Metamath Proof Explorer


Theorem alimdh

Description: Deduction form of Theorem 19.20 of Margaris p. 90, see alim . (Contributed by NM, 4-Jan-2002)

Ref Expression
Hypotheses alimdh.1 φ x φ
alimdh.2 φ ψ χ
Assertion alimdh φ x ψ x χ

Proof

Step Hyp Ref Expression
1 alimdh.1 φ x φ
2 alimdh.2 φ ψ χ
3 2 al2imi x φ x ψ x χ
4 1 3 syl φ x ψ x χ