Theorem 2albii 1827

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

Syntax hints:   ↔ wb 207  ∀wal 1545

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

This theorem depends on definitions:  df-bi 208

This theorem is referenced by:  3albii  1828  sbcom2  2183  2sb6rf  2481  mo4f  2571  2mo2  2651  2mos  2653  2mosOLD  2654  r3al  3178  ralcom  3268  ralcomf  3278  sbccomlem  3808  nfnid  5311  ssrel3  5736  raliunxp  5788  cnvsym  6071  intasym  6072  intirr  6075  codir  6077  qfto  6078  dfpo2  6254  dffun4  6505  fun11  6566  fununi  6567  mpo2eqb  7495  frpoins3xpg  8087  xpord3inddlem  8101  aceq0  10038  zfac  10380  zfcndac  10540  addsrmo  10994  mulsrmo  10995  cotr2g  14936  isirred2  20399  isdomn3  20694  ons2ind  28292  bnj580  35102  bnj978  35138  axacprim  35942  dfso2  35990  dfon2lem8  36023  dffun10  36147  mh-infprim2bi  36782  wl-sbcom2d  37939  mpobi123f  38536  r2alan  38625  inxpss  38691  inxpss3  38694  cnvref5  38725  trcoss2  38948  dfantisymrel5  39239  antisymrelres  39240  dford4  43481  undmrnresiss  44055  cnvssco  44057  pm14.12  44872  permac8prim  45465  ichn  47938  dfich2  47940  ichcom  47941  ichbi12i  47942  pg4cyclnex  48625