Metamath Proof Explorer
Description: Formulabuilding rule for universal quantifier (deduction form). See
also albidh and albid . (Contributed by NM, 26May1993)


Ref 
Expression 

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

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

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

ax5 
⊢ ( 𝜑 → ∀ 𝑥 𝜑 ) 
3 
2 1

albidh 
⊢ ( 𝜑 → ( ∀ 𝑥 𝜓 ↔ ∀ 𝑥 𝜒 ) ) 