Theorem 2albii 1820

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 1819	. 2 ⊢ (∀𝑦𝜑 ↔ ∀𝑦𝜓)
3	2	albii 1819	1 ⊢ (∀𝑥∀𝑦𝜑 ↔ ∀𝑥∀𝑦𝜓)

Syntax hints:   ↔ wb 206  ∀wal 1538

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  3albii  1821  sbcom2  2174  2sb6rf  2471  mo4f  2560  2mo2  2640  2mos  2642  2mosOLD  2643  r3al  3175  ralcom  3265  ralcomf  3276  sbccomlem  3832  nfnid  5330  ssrel3  5749  raliunxp  5803  cnvsym  6085  cnvsymOLD  6086  cnvsymOLDOLD  6087  intasym  6088  intirr  6091  codir  6093  qfto  6094  dfpo2  6269  dffun4  6527  fun11  6590  fununi  6591  mpo2eqb  7521  frpoins3xpg  8119  xpord3inddlem  8133  aceq0  10071  zfac  10413  zfcndac  10572  addsrmo  11026  mulsrmo  11027  cotr2g  14942  isirred2  20330  isdomn3  20624  bnj580  34903  bnj978  34939  axacprim  35694  dfso2  35742  dfon2lem8  35778  dffun10  35902  wl-sbcom2d  37549  mpobi123f  38156  r2alan  38238  inxpss  38299  inxpss3  38302  cnvref5  38333  trcoss2  38475  dfantisymrel5  38754  antisymrelres  38755  dford4  43018  undmrnresiss  43593  cnvssco  43595  pm14.12  44410  permac8prim  45004  ichn  47457  dfich2  47459  ichcom  47460  ichbi12i  47461  pg4cyclnex  48117