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  4921  cnvsym  5171  intasym  5172  intirr  5174  codir  5176  qfto  5177  dffun4  5388  dffun4f  5393  funcnveq  5444  fun11  5448  fununi  5449  mpo2eqb  6198  addnq0mo  7814  mulnq0mo  7815  addsrmo  8110  mulsrmo  8111