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  2176  2sb6rf  2473  mo4f  2562  2mo2  2642  2mos  2644  2mosOLD  2645  r3al  3170  ralcom  3260  ralcomf  3270  sbccomlem  3820  nfnid  5313  ssrel3  5726  raliunxp  5779  cnvsym  6061  intasym  6062  intirr  6065  codir  6067  qfto  6068  dfpo2  6243  dffun4  6494  fun11  6555  fununi  6556  mpo2eqb  7478  frpoins3xpg  8070  xpord3inddlem  8084  aceq0  10009  zfac  10351  zfcndac  10510  addsrmo  10964  mulsrmo  10965  cotr2g  14883  isirred2  20340  isdomn3  20631  bnj580  34923  bnj978  34959  axacprim  35749  dfso2  35797  dfon2lem8  35830  dffun10  35954  wl-sbcom2d  37601  mpobi123f  38208  r2alan  38290  inxpss  38351  inxpss3  38354  cnvref5  38385  trcoss2  38527  dfantisymrel5  38806  antisymrelres  38807  dford4  43068  undmrnresiss  43643  cnvssco  43645  pm14.12  44460  permac8prim  45053  ichn  47493  dfich2  47495  ichcom  47496  ichbi12i  47497  pg4cyclnex  48164