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 206  ∀wal 1540

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 207

This theorem is referenced by:  3albii  1823  sbcom2  2179  2sb6rf  2478  mo4f  2568  2mo2  2648  2mos  2650  2mosOLD  2651  r3al  3176  ralcom  3266  ralcomf  3276  sbccomlem  3821  nfnid  5322  ssrel3  5743  raliunxp  5796  cnvsym  6079  intasym  6080  intirr  6083  codir  6085  qfto  6086  dfpo2  6262  dffun4  6513  fun11  6574  fununi  6575  mpo2eqb  7500  frpoins3xpg  8092  xpord3inddlem  8106  aceq0  10040  zfac  10382  zfcndac  10542  addsrmo  10996  mulsrmo  10997  cotr2g  14911  isirred2  20369  isdomn3  20660  ons2ind  28283  bnj580  35088  bnj978  35124  axacprim  35920  dfso2  35968  dfon2lem8  36001  dffun10  36125  wl-sbcom2d  37813  mpobi123f  38410  r2alan  38499  inxpss  38565  inxpss3  38568  cnvref5  38599  trcoss2  38822  dfantisymrel5  39113  antisymrelres  39114  dford4  43383  undmrnresiss  43957  cnvssco  43959  pm14.12  44774  permac8prim  45367  ichn  47813  dfich2  47815  ichcom  47816  ichbi12i  47817  pg4cyclnex  48484