Theorem albii 1356

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

Syntax hints:   ↔ wb 98  ∀wal 1240

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 1333  ax-gen 1335

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  2albii  1357  hbxfrbi  1358  nfbii  1359  19.26-2  1368  19.26-3an  1369  alrot3  1371  alrot4  1372  albiim  1373  2albiim  1374  alnex  1385  nfalt  1467  aaanh  1475  aaan  1476  alinexa  1491  exintrbi  1521  19.21-2  1554  19.31r  1568  equsalh  1611  equsal  1612  sbcof2  1688  dvelimfALT2  1695  19.23vv  1761  sbanv  1766  pm11.53  1772  nfsbxy  1815  nfsbxyt  1816  sbcomxyyz  1843  sb9  1852  sbnf2  1854  2sb6  1857  sbcom2v  1858  sb6a  1861  2sb6rf  1863  sbalyz  1872  sbal  1873  sbal1yz  1874  sbal1  1875  sbalv  1878  2exsb  1882  nfsb4t  1887  dvelimf  1888  dveeq1  1892  sbal2  1895  sb8eu  1910  sb8euh  1920  eu1  1922  eu2  1941  mo3h  1950  moanim  1971  2eu4  1990  exists1  1993  eqcom  2039  hblem  2142  abeq2  2143  abeq1  2144  nfceqi  2171  abid2f  2199  ralbii2  2328  r2alf  2335  nfraldya  2352  r3al  2360  r19.21t  2388  r19.23t  2417  rabid2  2480  rabbi  2481  ralv  2565  ceqsralt  2575  gencbval  2596  ralab  2695  ralrab2  2700  euind  2722  reu2  2723  reu3  2725  rmo4  2728  reu8  2731  rmoim  2734  2reuswapdc  2737  reuind  2738  2rmorex  2739  ra5  2840  rmo2ilem  2841  rmo3  2843  dfss2  2928  ss2ab  3002  ss2rab  3010  rabss  3011  uniiunlem  3022  ssequn1  3107  unss  3111  ralunb  3118  ssin  3153  ssddif  3165  n0rf  3227  eq0  3233  eqv  3234  rabeq0  3241  abeq0  3242  disj  3262  disj3  3266  rgenm  3317  pwss  3366  ralsns  3399  disjsn  3423  euabsn2  3430  snss  3485  snsssn  3523  dfnfc2  3589  uni0b  3596  unissb  3601  elintrab  3618  ssintrab  3629  intun  3637  intpr  3638  dfiin2g  3681  iunss  3689  dfdisj2  3738  cbvdisj  3746  dftr2  3847  dftr5  3848  trint  3860  zfnuleu  3872  vprc  3879  inex1  3882  repizf2lem  3905  axpweq  3915  zfpow  3919  axpow2  3920  axpow3  3921  zfpair2  3936  ssextss  3947  sucel  4113  zfun  4137  uniex2  4139  setindel  4221  setind  4222  elirr  4224  en2lp  4232  tfi  4248  peano5  4264  ssrel  4371  ssrel2  4373  eqrelrel  4384  reliun  4401  raliunxp  4420  relop  4429  dmopab3  4491  dm0rn0  4495  reldm0  4496  cotr  4649  issref  4650  asymref  4653  intirr  4654  sb8iota  4817  dffun2  4855  dffun4  4856  dffun6f  4858  dffun4f  4861  dffun7  4871  funopab  4878  funcnv2  4902  funcnv  4903  funcnveq  4905  fun2cnv  4906  fun11  4909  fununi  4910  funcnvuni  4911  funimaexglem  4925  fnres  4958  fnopabg  4965  rexrnmpt  5253  dff13  5350  oprabidlem  5479  eqoprab2b  5505  mpt22eqb  5552  ralrnmpt2  5557  dfer2  6043  ltexprlemdisj  6579  recexprlemdisj  6601  bj-nfalt  9219  bdceq  9277  bdcriota  9318  bj-vprc  9327  bdinex1  9330  bj-zfpair2  9341  bj-uniex2  9347  bj-ssom  9370  peano5set  9374  bj-inf2vnlem2  9401