Theorem 2albii 1853

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

This proof depends on syntax axioms:   ↔ wb 209  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210

This theorem is used by:  3albii  1854  sbcom2  2212  2sb6rf  2505  mo4f  2595  2mo2  2675  2mos  2677  r3al  3204  ralcom  3294  ralcomf  3304  sbccomlem  3821  nfnid  5344  ssrel3  5771  raliunxp  5826  cnvsym  6126  intasym  6127  intirr  6130  codir  6132  qfto  6133  dfpo2  6325  dffun4  6579  fun11  6644  fununi  6645  mpo2eqb  7583  frpoins3xpg  8194  xpord3inddlem  8208  aceq0  10236  zfac  10577  zfcndac  10743  addsrmo  11197  mulsrmo  11198  cotr2g  15172  isirred2  20702  isdomn3  21017  ons2ind  28718  bnj580  35654  bnj978  35690  axacprim  36687  dfso2  36735  dfon2lem8  36767  dffun10  36891  mh-infprim2bi  37550  wl-sbcom2d  38761  mpobi123f  39360  r2alan  39449  inxpss  39515  inxpss3  39518  cnvref5  39549  trcoss2  39772  dfantisymrel5  40063  antisymrelres  40064  dford4  44302  undmrnresiss  44865  cnvssco  44867  pm14.12  45665  permac8prim  46268  ichn  48811  dfich2  48813  ichcom  48814  ichbi12i  48815  pg4cyclnex  49498