Metamath Proof Explorer
Description: Formulabuilding rule for two universal quantifiers (deduction form).
(Contributed by NM, 4Mar1997)


Ref 
Expression 

Hypothesis 
2albidv.1 
⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) ) 

Assertion 
2albidv 
⊢ ( 𝜑 → ( ∀ 𝑥 ∀ 𝑦 𝜓 ↔ ∀ 𝑥 ∀ 𝑦 𝜒 ) ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

2albidv.1 
⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) ) 
2 
1

albidv 
⊢ ( 𝜑 → ( ∀ 𝑦 𝜓 ↔ ∀ 𝑦 𝜒 ) ) 
3 
2

albidv 
⊢ ( 𝜑 → ( ∀ 𝑥 ∀ 𝑦 𝜓 ↔ ∀ 𝑥 ∀ 𝑦 𝜒 ) ) 