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  3808  nfnid  5312  ssrel3  5735  raliunxp  5788  cnvsym  6071  intasym  6072  intirr  6075  codir  6077  qfto  6078  dfpo2  6254  dffun4  6505  fun11  6566  fununi  6567  mpo2eqb  7492  frpoins3xpg  8083  xpord3inddlem  8097  aceq0  10031  zfac  10373  zfcndac  10533  addsrmo  10987  mulsrmo  10988  cotr2g  14929  isirred2  20392  isdomn3  20683  ons2ind  28281  bnj580  35071  bnj978  35107  axacprim  35905  dfso2  35953  dfon2lem8  35986  dffun10  36110  mh-infprim2bi  36745  wl-sbcom2d  37900  mpobi123f  38497  r2alan  38586  inxpss  38652  inxpss3  38655  cnvref5  38686  trcoss2  38909  dfantisymrel5  39200  antisymrelres  39201  dford4  43475  undmrnresiss  44049  cnvssco  44051  pm14.12  44866  permac8prim  45459  ichn  47928  dfich2  47930  ichcom  47931  ichbi12i  47932  pg4cyclnex  48615