Theorem 2albii 1839

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

Syntax hints:   ↔ wb 208  ∀wal 1557

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

This theorem depends on definitions:  df-bi 209

This theorem is referenced by:  3albii  1840  sbcom2  2205  2sb6rf  2503  mo4f  2593  2mo2  2673  2mos  2675  r3al  3199  ralcom  3289  ralcomf  3299  sbccomlem  3820  nfnid  5329  ssrel3  5754  raliunxp  5807  cnvsym  6096  intasym  6097  intirr  6100  codir  6102  qfto  6103  dfpo2  6277  dffun4  6528  fun11  6589  fununi  6590  mpo2eqb  7522  frpoins3xpg  8113  xpord3inddlem  8127  aceq0  10067  zfac  10410  zfcndac  10570  addsrmo  11024  mulsrmo  11025  cotr2g  14982  isirred2  20456  isdomn3  20751  ons2ind  28355  bnj580  35168  bnj978  35204  axacprim  36017  dfso2  36065  dfon2lem8  36098  dffun10  36222  mh-infprim2bi  36867  wl-sbcom2d  38024  mpobi123f  38621  r2alan  38710  inxpss  38776  inxpss3  38779  cnvref5  38810  trcoss2  39033  dfantisymrel5  39324  antisymrelres  39325  dford4  43566  undmrnresiss  44140  cnvssco  44142  pm14.12  44957  permac8prim  45550  ichn  48022  dfich2  48024  ichcom  48025  ichbi12i  48026  pg4cyclnex  48709