Metamath Proof Explorer


Theorem exlimivv

Description: Inference form of Theorem 19.23 of Margaris p. 90, see 19.23 . (Contributed by NM, 1-Aug-1995)

Ref Expression
Hypothesis exlimivv.1 φψ
Assertion exlimivv xyφψ

Proof

Step Hyp Ref Expression
1 exlimivv.1 φψ
2 1 exlimiv yφψ
3 2 exlimiv xyφψ