Metamath Proof Explorer


Theorem exlimd

Description: Deduction form of Theorem 19.9 of Margaris p. 89. (Contributed by NM, 23-Jan-1993) (Revised by Mario Carneiro, 24-Sep-2016) (Proof shortened by Wolf Lammen, 12-Jan-2018)

Ref Expression
Hypotheses exlimd.1 x φ
exlimd.2 x χ
exlimd.3 φ ψ χ
Assertion exlimd φ x ψ χ

Proof

Step Hyp Ref Expression
1 exlimd.1 x φ
2 exlimd.2 x χ
3 exlimd.3 φ ψ χ
4 1 3 eximd φ x ψ x χ
5 2 19.9 x χ χ
6 4 5 syl6ib φ x ψ χ