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  33924  bnj978  33960  axacprim  34676  dfso2  34725  dfon2lem8  34762  dffun10  34886  wl-sbcom2d  36426  mpobi123f  37030  r2alan  37116  inxpss  37180  inxpss3  37183  cnvref5  37220  trcoss2  37354  dfantisymrel5  37632  antisymrelres  37633  dford4  41768  isdomn3  41946  undmrnresiss  42355  cnvssco  42357  pm14.12  43180  ichn  46124  dfich2  46126  ichcom  46127  ichbi12i  46128