Metamath Proof Explorer

Theorem alrimivv

Description: Inference form of Theorem 19.21 of Margaris p. 90. See 19.21 and 19.21v . (Contributed by NM, 31-Jul-1995)

Ref Expression
Hypothesis alrimivv.1 φ ψ
Assertion alrimivv φ x y ψ


Step Hyp Ref Expression
1 alrimivv.1 φ ψ
2 1 alrimiv φ y ψ
3 2 alrimiv φ x y ψ