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ψχ