Theorem albii 1335

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 1333	. 2 ⊢ (∀x(φ ↔ ψ) → (∀xφ ↔ ∀xψ))
2		albii.1	. 2 ⊢ (φ ↔ ψ)
3	1, 2	mpg 1316	1 ⊢ (∀xφ ↔ ∀xψ)

Syntax hints:   ↔ wb 98  ∀wal 1224

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 1312  ax-gen 1314

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  2albii  1336  hbxfrbi  1337  nfbii  1338  19.26-2  1347  19.26-3an  1348  alrot3  1350  alrot4  1351  alrot4OLD  1352  albiim  1353  2albiim  1354  alnex  1365  nfalt  1448  aaanh  1456  aaan  1457  alinexa  1472  exintrbi  1502  19.21-2  1535  19.31r  1549  equsalh  1592  equsal  1593  sbcof2  1669  dvelimfALT2  1676  19.23vv  1742  sbanv  1747  pm11.53  1753  nfsbxy  1796  nfsbxyt  1797  sbcomxyyz  1824  sb9  1833  sbnf2  1835  2sb6  1838  sbcom2v  1839  sb6a  1842  2sb6rf  1844  sbalyz  1853  sbal  1854  sbal1yz  1855  sbal1  1856  sbalv  1859  2exsb  1863  nfsb4t  1868  dvelimf  1869  dveeq1  1873  sbal2  1876  sb8eu  1891  sb8euh  1901  eu1  1903  eu2  1922  mo3h  1931  moanim  1952  2eu4  1971  exists1  1974  eqcom  2020  hblem  2123  abeq2  2124  abeq1  2125  nfceqi  2152  abid2f  2180  ralbii2  2308  r2alf  2315  nfraldya  2332  r3al  2340  r19.21t  2368  r19.23t  2397  rabid2  2460  rabbi  2461  ralv  2544  ceqsralt  2554  gencbval  2575  ralab  2674  ralrab2  2679  euind  2701  reu2  2702  reu3  2704  rmo4  2707  reu8  2710  rmoim  2713  2reuswapdc  2716  reuind  2717  2rmorex  2718  ra5  2819  rmo2ilem  2820  rmo3  2822  dfss2  2907  ss2ab  2981  ss2rab  2989  rabss  2990  uniiunlem  3001  ssequn1  3086  unss  3090  ralunb  3097  ssin  3132  ssddif  3144  n0rf  3206  eq0  3212  eqv  3213  rabeq0  3220  abeq0  3221  disj  3241  disj3  3245  rgenm  3298  pwss  3345  ralsns  3378  disjsn  3402  euabsn2  3409  snss  3464  snsssn  3502  dfnfc2  3568  uni0b  3575  unissb  3580  elintrab  3597  ssintrab  3608  intun  3616  intpr  3617  dfiin2g  3660  iunss  3668  dfdisj2  3717  cbvdisj  3725  dftr2  3826  dftr5  3827  trint  3839  zfnuleu  3851  vprc  3858  inex1  3861  repizf2lem  3884  axpweq  3894  zfpow  3898  axpow2  3899  axpow3  3900  zfpair2  3915  ssextss  3926  sucel  4092  zfun  4117  uniex2  4119  setindel  4201  setind  4202  elirr  4204  en2lp  4212  tfi  4228  peano5  4244  ssrel  4351  ssrel2  4353  eqrelrel  4364  reliun  4381  raliunxp  4400  relop  4409  dmopab3  4471  dm0rn0  4475  reldm0  4476  cotr  4629  issref  4630  asymref  4633  intirr  4634  sb8iota  4797  dffun2  4835  dffun4  4836  dffun6f  4837  dffun4f  4840  dffun7  4850  funopab  4857  funcnv2  4881  funcnv  4882  funcnveq  4884  fun2cnv  4885  fun11  4888  fununi  4889  funcnvuni  4890  funimaexglem  4904  fnres  4937  fnopabg  4944  rexrnmpt  5231  dff13  5328  oprabidlem  5456  eqoprab2b  5482  mpt22eqb  5529  ralrnmpt2  5534  dfer2  6014  ltexprlemdisj  6437  recexprlemdisj  6458  bj-nfalt  7150  bdceq  7208  bdcriota  7249  bj-vprc  7258  bdinex1  7261  bj-zfpair2  7272  bj-uniex2  7278  bj-ssom  7297  peano5set  7301  bj-inf2vnlem2  7328