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


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