Theorem albii 1332

Description: Inference adding universal quantifier to both sides of an equivalence. (Contributed by NM, 7-Aug-1994.)

Hypothesis

Ref	Expression
albii.1	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
albii	⊢ (∀xφ ↔ ∀xψ)

Proof of Theorem albii

Step	Hyp	Ref	Expression
1		albi 1330	. 2 ⊢ (∀x(φ ↔ ψ) → (∀xφ ↔ ∀xψ))
2		albii.1	. 2 ⊢ (φ ↔ ψ)
3	1, 2	mpg 1313	1 ⊢ (∀xφ ↔ ∀xψ)

Syntax hints:   ↔ wb 98  ∀wal 1221

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1309  ax-gen 1311

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  2albii  1333  hbxfrbi  1334  nfbii  1335  19.26-2  1344  19.26-3an  1345  alrot3  1347  alrot4  1348  albiim  1349  2albiim  1350  alnex  1361  nfalt  1443  aaanh  1451  aaan  1452  alinexa  1467  exintrbi  1497  19.21-2  1530  19.31r  1544  equsalh  1587  equsal  1588  sbcof2  1664  dvelimfALT2  1671  19.23vv  1737  sbanv  1742  pm11.53  1748  nfsbxy  1791  nfsbxyt  1792  sbcomxyyz  1819  sb9  1828  sbnf2  1830  2sb6  1833  sbcom2v  1834  sb6a  1837  2sb6rf  1839  sbalyz  1848  sbal  1849  sbal1yz  1850  sbal1  1851  sbalv  1854  2exsb  1858  nfsb4t  1863  dvelimf  1864  dveeq1  1868  sbal2  1871  sb8eu  1886  sb8euh  1896  eu1  1898  eu2  1917  mo3h  1926  moanim  1947  2eu4  1966  exists1  1969  eqcom  2015  hblem  2118  abeq2  2119  abeq1  2120  nfceqi  2147  abid2f  2175  ralbii2  2303  r2alf  2310  nfraldya  2327  r3al  2335  r19.21t  2363  r19.23t  2392  rabid2  2455  rabbi  2456  ralv  2539  ceqsralt  2549  gencbval  2570  ralab  2669  ralrab2  2674  euind  2696  reu2  2697  reu3  2699  rmo4  2702  reu8  2705  rmoim  2708  2reuswapdc  2711  reuind  2712  2rmorex  2713  ra5  2814  rmo2ilem  2815  rmo3  2817  dfss2  2902  ss2ab  2976  ss2rab  2984  rabss  2985  uniiunlem  2996  ssequn1  3081  unss  3085  ralunb  3092  ssin  3127  ssddif  3139  n0rf  3201  eq0  3207  eqv  3208  rabeq0  3215  abeq0  3216  disj  3236  disj3  3240  rgenm  3291  pwss  3338  ralsns  3371  disjsn  3395  euabsn2  3402  snss  3457  snsssn  3495  dfnfc2  3561  uni0b  3568  unissb  3573  elintrab  3590  ssintrab  3601  intun  3609  intpr  3610  dfiin2g  3653  iunss  3661  dfdisj2  3710  cbvdisj  3718  dftr2  3819  dftr5  3820  trint  3832  zfnuleu  3844  vprc  3851  inex1  3854  repizf2lem  3877  axpweq  3887  zfpow  3891  axpow2  3892  axpow3  3893  zfpair2  3908  ssextss  3919  sucel  4085  zfun  4109  uniex2  4111  setindel  4193  setind  4194  elirr  4196  en2lp  4204  tfi  4220  peano5  4236  ssrel  4343  ssrel2  4345  eqrelrel  4356  reliun  4373  raliunxp  4392  relop  4401  dmopab3  4463  dm0rn0  4467  reldm0  4468  cotr  4621  issref  4622  asymref  4625  intirr  4626  sb8iota  4789  dffun2  4827  dffun4  4828  dffun6f  4829  dffun4f  4832  dffun7  4842  funopab  4849  funcnv2  4873  funcnv  4874  funcnveq  4876  fun2cnv  4877  fun11  4880  fununi  4881  funcnvuni  4882  funimaexglem  4896  fnres  4929  fnopabg  4936  rexrnmpt  5223  dff13  5320  oprabidlem  5448  eqoprab2b  5474  mpt22eqb  5521  ralrnmpt2  5526  dfer2  6006  ltexprlemdisj  6429  recexprlemdisj  6451  bj-nfalt  8169  bdceq  8227  bdcriota  8268  bj-vprc  8277  bdinex1  8280  bj-zfpair2  8291  bj-uniex2  8297  bj-ssom  8320  peano5set  8324  bj-inf2vnlem2  8351