Theorem 2albii 1823

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

Syntax hints:   ↔ wb 205  ∀wal 1540

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

This theorem depends on definitions:  df-bi 206

This theorem is referenced by:  3albii  1824  sbcom2  2162  2sb6rf  2473  mo4f  2562  2mo2  2644  2mos  2646  r3al  3197  ralcom  3287  ralcomf  3300  nfnid  5374  ssrel3  5787  raliunxp  5840  cnvsym  6114  cnvsymOLD  6115  cnvsymOLDOLD  6116  intasym  6117  intirr  6120  codir  6122  qfto  6123  dfpo2  6296  dffun4  6560  fun11  6623  fununi  6624  mpo2eqb  7541  frpoins3xpg  8126  xpord3inddlem  8140  aceq0  10113  zfac  10455  zfcndac  10614  addsrmo  11068  mulsrmo  11069  cotr2g  14923  isirred2  20235  bnj580  33955  bnj978  33991  axacprim  34707  dfso2  34756  dfon2lem8  34793  dffun10  34917  wl-sbcom2d  36474  mpobi123f  37078  r2alan  37164  inxpss  37228  inxpss3  37231  cnvref5  37268  trcoss2  37402  dfantisymrel5  37680  antisymrelres  37681  dford4  41816  isdomn3  41994  undmrnresiss  42403  cnvssco  42405  pm14.12  43228  ichn  46172  dfich2  46174  ichcom  46175  ichbi12i  46176