Metamath Proof Explorer

Theorem eximdv

Description: Deduction form of Theorem 19.22 of Margaris p. 90, see exim . See eximdh and eximd for versions without a distinct variable condition. (Contributed by NM, 27-Apr-1994)

Ref Expression
Hypothesis alimdv.1 φ ψ χ
Assertion eximdv φ x ψ x χ


Step Hyp Ref Expression
1 alimdv.1 φ ψ χ
2 ax-5 φ x φ
3 2 1 eximdh φ x ψ x χ