Theorem 2albii 1816

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

Syntax hints:   ↔ wb 206  ∀wal 1534

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  3albii  1817  sbcom2  2170  2sb6rf  2475  mo4f  2564  2mo2  2644  2mos  2646  2mosOLD  2647  r3al  3194  ralcom  3286  ralcomf  3299  sbccomlem  3877  nfnid  5380  ssrel3  5798  raliunxp  5852  cnvsym  6134  cnvsymOLD  6135  cnvsymOLDOLD  6136  intasym  6137  intirr  6140  codir  6142  qfto  6143  dfpo2  6317  dffun4  6578  fun11  6641  fununi  6642  mpo2eqb  7564  frpoins3xpg  8163  xpord3inddlem  8177  aceq0  10155  zfac  10497  zfcndac  10656  addsrmo  11110  mulsrmo  11111  cotr2g  15011  isirred2  20437  isdomn3  20731  bnj580  34905  bnj978  34941  axacprim  35686  dfso2  35734  dfon2lem8  35771  dffun10  35895  wl-sbcom2d  37541  mpobi123f  38148  r2alan  38230  inxpss  38292  inxpss3  38295  cnvref5  38332  trcoss2  38465  dfantisymrel5  38743  antisymrelres  38744  dford4  43017  undmrnresiss  43593  cnvssco  43595  pm14.12  44416  ichn  47380  dfich2  47382  ichcom  47383  ichbi12i  47384