Metamath Proof Explorer
Description: Inference removing two universal quantifiers. Version of 19.21bi with
two quantifiers. (Contributed by NM, 20Apr1994)


Ref 
Expression 

Hypothesis 
19.21bbi.1 
⊢ ( 𝜑 → ∀ 𝑥 ∀ 𝑦 𝜓 ) 

Assertion 
19.21bbi 
⊢ ( 𝜑 → 𝜓 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

19.21bbi.1 
⊢ ( 𝜑 → ∀ 𝑥 ∀ 𝑦 𝜓 ) 
2 
1

19.21bi 
⊢ ( 𝜑 → ∀ 𝑦 𝜓 ) 
3 
2

19.21bi 
⊢ ( 𝜑 → 𝜓 ) 