Theorem 2albii 1822

Description: Inference adding two 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 1821	. 2 ⊢ (∀𝑦𝜑 ↔ ∀𝑦𝜓)
3	2	albii 1821	1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓)

Syntax hints:   ↔ wb 209  ∀wal 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811

This theorem depends on definitions:  df-bi 210

This theorem is referenced by:  sbcom2  2165  2sb6rf  2486  mo4f  2626  2mo2  2709  2mos  2711  r3al  3167  ralcom  3307  ralcomf  3310  nfnid  5241  raliunxp  5674  cnvsym  5941  intasym  5942  intirr  5945  codir  5947  qfto  5948  dffun4  6336  fun11  6398  fununi  6399  mpo2eqb  7262  aceq0  9529  zfac  9871  zfcndac  10030  addsrmo  10484  mulsrmo  10485  cotr2g  14327  isirred2  19447  bnj580  32295  bnj978  32331  axacprim  33046  dfso2  33103  dfpo2  33104  dfon2lem8  33148  dffun10  33488  wl-sbcom2d  34962  mpobi123f  35600  3albii  35669  ssrel3  35716  inxpss  35729  inxpss3  35731  trcoss2  35884  dford4  39970  isdomn3  40148  undmrnresiss  40304  cnvssco  40306  pm14.12  41125  ichn  43973  dfich2  43975  ichcom  43976  ichbi12i  43977