Metamath Proof Explorer


Theorem alimd

Description: Deduction form of Theorem 19.20 of Margaris p. 90, see alim . See alimdh , alimdv for variants requiring fewer axioms. (Contributed by Mario Carneiro, 24-Sep-2016)

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

Proof

Step Hyp Ref Expression
1 alimd.1 x φ
2 alimd.2 φ ψ χ
3 1 nf5ri φ x φ
4 3 2 alimdh φ x ψ x χ