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 x y φ ψ


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