Theorem 2albii 1853

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

This proof depends on syntax axioms:   ↔ wb 209  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210

This theorem is used by:  3albii  1854  sbcom2  2210  2sb6rf  2507  mo4f  2597  2mo2  2677  2mos  2679  r3al  3205  ralcom  3295  ralcomf  3305  sbccomlem  3824  nfnid  5348  ssrel3  5774  raliunxp  5827  cnvsym  6116  intasym  6117  intirr  6120  codir  6122  qfto  6123  dfpo2  6301  dffun4  6553  fun11  6614  fununi  6615  mpo2eqb  7548  frpoins3xpg  8138  xpord3inddlem  8152  aceq0  10114  zfac  10455  zfcndac  10615  addsrmo  11069  mulsrmo  11070  cotr2g  15032  isirred2  20528  isdomn3  20842  ons2ind  28497  bnj580  35325  bnj978  35361  axacprim  36212  dfso2  36260  dfon2lem8  36293  dffun10  36417  mh-infprim2bi  37091  wl-sbcom2d  38249  mpobi123f  38844  r2alan  38933  inxpss  38999  inxpss3  39002  cnvref5  39033  trcoss2  39256  dfantisymrel5  39547  antisymrelres  39548  dford4  43789  undmrnresiss  44363  cnvssco  44365  pm14.12  45164  permac8prim  45756  ichn  48238  dfich2  48240  ichcom  48241  ichbi12i  48242  pg4cyclnex  48925