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  2475  mo4f  2564  2mo2  2644  2mos  2646  2mosOLD  2647  r3al  3171  ralcom  3261  ralcomf  3271  sbccomlem  3816  nfnid  5317  ssrel3  5732  raliunxp  5785  cnvsym  6067  intasym  6068  intirr  6071  codir  6073  qfto  6074  dfpo2  6250  dffun4  6501  fun11  6562  fununi  6563  mpo2eqb  7486  frpoins3xpg  8078  xpord3inddlem  8092  aceq0  10018  zfac  10360  zfcndac  10519  addsrmo  10973  mulsrmo  10974  cotr2g  14887  isirred2  20343  isdomn3  20634  bnj580  34948  bnj978  34984  axacprim  35774  dfso2  35822  dfon2lem8  35855  dffun10  35979  wl-sbcom2d  37628  mpobi123f  38225  r2alan  38309  inxpss  38372  inxpss3  38375  cnvref5  38406  trcoss2  38609  dfantisymrel5  38883  antisymrelres  38884  dford4  43149  undmrnresiss  43724  cnvssco  43726  pm14.12  44541  permac8prim  45134  ichn  47583  dfich2  47585  ichcom  47586  ichbi12i  47587  pg4cyclnex  48254