Theorem 2albii 1524

Description: Inference adding 2 universal quantifiers to both sides of an equivalence. (Contributed by NM, 9-Mar-1997.)

Hypothesis

Ref	Expression
albii.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
2albii	⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓)

Proof of Theorem 2albii

Step	Hyp	Ref	Expression
1		albii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	albii 1523	. 2 ⊢ (∀𝑦𝜑 ↔ ∀𝑦𝜓)
3	2	albii 1523	1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓)

This proof depends on syntax axioms:   ↔ wb 105  ∀wal 1400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502

This proof depends on definitions:  df-bi 117

This theorem is used by:  mor  2129  mo4f  2147  moanim  2161  2eu4  2180  ralcomf  2712  raliunxp  4923  cnvsym  5174  intasym  5175  intirr  5177  codir  5179  qfto  5180  dffun4  5391  dffun4f  5396  funcnveq  5447  fun11  5451  fununi  5452  mpo2eqb  6201  addnq0mo  7820  mulnq0mo  7821  addsrmo  8116  mulsrmo  8117