Theorem 2albii 1821

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

Syntax hints:   ↔ wb 206  ∀wal 1539

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  3albii  1822  sbcom2  2178  2sb6rf  2477  mo4f  2567  2mo2  2647  2mos  2649  2mosOLD  2650  r3al  3174  ralcom  3264  ralcomf  3274  sbccomlem  3819  nfnid  5320  ssrel3  5735  raliunxp  5788  cnvsym  6071  intasym  6072  intirr  6075  codir  6077  qfto  6078  dfpo2  6254  dffun4  6505  fun11  6566  fununi  6567  mpo2eqb  7490  frpoins3xpg  8082  xpord3inddlem  8096  aceq0  10028  zfac  10370  zfcndac  10530  addsrmo  10984  mulsrmo  10985  cotr2g  14899  isirred2  20357  isdomn3  20648  ons2ind  28271  bnj580  35069  bnj978  35105  axacprim  35901  dfso2  35949  dfon2lem8  35982  dffun10  36106  wl-sbcom2d  37766  mpobi123f  38363  r2alan  38447  inxpss  38510  inxpss3  38513  cnvref5  38544  trcoss2  38747  dfantisymrel5  39021  antisymrelres  39022  dford4  43271  undmrnresiss  43845  cnvssco  43847  pm14.12  44662  permac8prim  45255  ichn  47702  dfich2  47704  ichcom  47705  ichbi12i  47706  pg4cyclnex  48373