Metamath Proof Explorer


Theorem exlimdv

Description: Deduction form of Theorem 19.23 of Margaris p. 90, see 19.23 . (Contributed by NM, 27-Apr-1994) Remove dependencies on ax-6 , ax-7 . (Revised by Wolf Lammen, 4-Dec-2017)

Ref Expression
Hypothesis exlimdv.1 φψχ
Assertion exlimdv φxψχ

Proof

Step Hyp Ref Expression
1 exlimdv.1 φψχ
2 1 eximdv φxψxχ
3 ax5e xχχ
4 2 3 syl6 φxψχ