Metamath Proof Explorer

Theorem 19.21bbi

Description: Inference removing two universal quantifiers. Version of 19.21bi with two quantifiers. (Contributed by NM, 20-Apr-1994)

Ref Expression
Hypothesis 19.21bbi.1 φ x y ψ
Assertion 19.21bbi φ ψ


Step Hyp Ref Expression
1 19.21bbi.1 φ x y ψ
2 1 19.21bi φ y ψ
3 2 19.21bi φ ψ