Theorem 2albii 1820

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

Syntax hints:   ↔ wb 206  ∀wal 1538

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

This theorem depends on definitions:  df-bi 207

This theorem is referenced by:  3albii  1821  sbcom2  2174  2sb6rf  2472  mo4f  2561  2mo2  2641  2mos  2643  2mosOLD  2644  r3al  3176  ralcom  3266  ralcomf  3278  sbccomlem  3835  nfnid  5333  ssrel3  5752  raliunxp  5806  cnvsym  6088  cnvsymOLD  6089  cnvsymOLDOLD  6090  intasym  6091  intirr  6094  codir  6096  qfto  6097  dfpo2  6272  dffun4  6530  fun11  6593  fununi  6594  mpo2eqb  7524  frpoins3xpg  8122  xpord3inddlem  8136  aceq0  10078  zfac  10420  zfcndac  10579  addsrmo  11033  mulsrmo  11034  cotr2g  14949  isirred2  20337  isdomn3  20631  bnj580  34910  bnj978  34946  axacprim  35701  dfso2  35749  dfon2lem8  35785  dffun10  35909  wl-sbcom2d  37556  mpobi123f  38163  r2alan  38245  inxpss  38306  inxpss3  38309  cnvref5  38340  trcoss2  38482  dfantisymrel5  38761  antisymrelres  38762  dford4  43025  undmrnresiss  43600  cnvssco  43602  pm14.12  44417  permac8prim  45011  ichn  47461  dfich2  47463  ichcom  47464  ichbi12i  47465  pg4cyclnex  48121