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 205  ∀wal 1539

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 206

This theorem is referenced by:  3albii  1823  sbcom2  2161  2sb6rf  2472  mo4f  2561  2mo2  2643  2mos  2645  r3al  3196  ralcom  3286  ralcomf  3299  nfnid  5373  ssrel3  5786  raliunxp  5839  cnvsym  6113  cnvsymOLD  6114  cnvsymOLDOLD  6115  intasym  6116  intirr  6119  codir  6121  qfto  6122  dfpo2  6295  dffun4  6559  fun11  6622  fununi  6623  mpo2eqb  7543  frpoins3xpg  8128  xpord3inddlem  8142  aceq0  10115  zfac  10457  zfcndac  10616  addsrmo  11070  mulsrmo  11071  cotr2g  14927  isirred2  20312  bnj580  34210  bnj978  34246  axacprim  34968  dfso2  35017  dfon2lem8  35054  dffun10  35178  wl-sbcom2d  36729  mpobi123f  37333  r2alan  37419  inxpss  37483  inxpss3  37486  cnvref5  37523  trcoss2  37657  dfantisymrel5  37935  antisymrelres  37936  dford4  42070  isdomn3  42248  undmrnresiss  42657  cnvssco  42659  pm14.12  43482  ichn  46423  dfich2  46425  ichcom  46426  ichbi12i  46427