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 206  ∀wal 1540

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 207

This theorem is referenced by:  3albii  1823  sbcom2  2179  2sb6rf  2477  mo4f  2567  2mo2  2647  2mos  2649  2mosOLD  2650  r3al  3175  ralcom  3265  ralcomf  3275  sbccomlem  3807  nfnid  5317  ssrel3  5742  raliunxp  5794  cnvsym  6077  intasym  6078  intirr  6081  codir  6083  qfto  6084  dfpo2  6260  dffun4  6511  fun11  6572  fununi  6573  mpo2eqb  7499  frpoins3xpg  8090  xpord3inddlem  8104  aceq0  10040  zfac  10382  zfcndac  10542  addsrmo  10996  mulsrmo  10997  cotr2g  14938  isirred2  20401  isdomn3  20692  ons2ind  28267  bnj580  35055  bnj978  35091  axacprim  35889  dfso2  35937  dfon2lem8  35970  dffun10  36094  mh-infprim2bi  36729  wl-sbcom2d  37886  mpobi123f  38483  r2alan  38572  inxpss  38638  inxpss3  38641  cnvref5  38672  trcoss2  38895  dfantisymrel5  39186  antisymrelres  39187  dford4  43457  undmrnresiss  44031  cnvssco  44033  pm14.12  44848  permac8prim  45441  ichn  47916  dfich2  47918  ichcom  47919  ichbi12i  47920  pg4cyclnex  48603