Theorem albii 1447

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

Hypothesis

Ref	Expression
albii.1	|- ( ph <-> ps )

Assertion

Ref	Expression
albii	|- ( A. x ph <-> A. x ps )

Proof of Theorem albii

Step	Hyp	Ref	Expression
1		albi 1445	. 2 |- ( A. x ( ph <-> ps ) -> ( A. x ph <-> A. x ps ) )
2		albii.1	. 2 |- ( ph <-> ps )
3	1, 2	mpg 1428	1 |- ( A. x ph <-> A. x ps )

Syntax hints:   <-> wb 104   A.wal 1330

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2albii  1448  hbxfrbi  1449  nfbii  1450  19.26-2  1459  19.26-3an  1460  alrot3  1462  alrot4  1463  albiim  1464  2albiim  1465  alnex  1476  nfalt  1555  aaanh  1563  aaan  1564  alinexa  1580  exintrbi  1610  19.21-2  1644  19.31r  1658  equsalh  1703  equsal  1704  equsalv  1770  sbcof2  1787  dvelimfALT2  1794  19.23vv  1861  sbanv  1866  pm11.53  1872  nfsbxy  1919  nfsbxyt  1920  sbcomxyyz  1949  sb9  1956  sbnf2  1958  2sb6  1961  sbcom2v  1962  sb6a  1965  2sb6rf  1967  sbalyz  1976  sbal  1977  sbal1yz  1978  sbal1  1979  sbalv  1982  2exsb  1986  nfsb4t  1991  dvelimf  1992  dveeq1  1996  sbal2  1997  sb8eu  2016  sb8euh  2026  eu1  2028  eu2  2047  mo3h  2056  moanim  2077  2eu4  2096  exists1  2099  eqcom  2156  hblem  2262  abeq2  2263  abeq1  2264  nfceqi  2292  abid2f  2322  dfrex2dc  2445  ralbii2  2464  r2alf  2471  nfraldya  2489  r3al  2498  r19.21t  2529  r19.23t  2561  rabid2  2630  rabbi  2631  ralv  2726  ceqsralt  2736  gencbval  2757  rspc2gv  2825  ralab  2868  ralrab2  2873  euind  2895  reu2  2896  reu3  2898  rmo4  2901  reu8  2904  rmo3f  2905  rmoim  2909  2reuswapdc  2912  reuind  2913  2rmorex  2914  ra5  3021  rmo2ilem  3022  rmo3  3024  dfss2  3113  ss2ab  3192  ss2rab  3200  rabss  3201  uniiunlem  3212  dfdif3  3213  ddifstab  3235  ssequn1  3273  unss  3277  ralunb  3284  ssin  3325  ssddif  3337  n0rf  3402  eq0  3408  eqv  3409  rabeq0  3419  abeq0  3420  disj  3438  disj3  3442  rgenm  3492  pwss  3555  ralsnsg  3592  ralsns  3593  disjsn  3617  euabsn2  3624  snss  3681  snsssn  3720  dfnfc2  3786  uni0b  3793  unissb  3798  elintrab  3815  ssintrab  3826  intun  3834  intpr  3835  dfiin2g  3878  iunss  3886  dfdisj2  3940  cbvdisj  3948  disjnim  3952  dftr2  4060  dftr5  4061  trint  4073  zfnuleu  4084  vnex  4091  inex1  4094  repizf2lem  4117  axpweq  4127  zfpow  4131  axpow2  4132  axpow3  4133  exmid01  4154  zfpair2  4165  ssextss  4175  frirrg  4305  sucel  4365  zfun  4389  uniex2  4391  setindel  4491  setind  4492  elirr  4494  en2lp  4507  zfregfr  4527  tfi  4535  peano5  4551  ssrel  4667  ssrel2  4669  eqrelrel  4680  reliun  4700  raliunxp  4720  relop  4729  dmopab3  4792  dm0rn0  4796  reldm0  4797  cotr  4960  issref  4961  asymref  4964  intirr  4965  sb8iota  5135  dffun2  5173  dffun4  5174  dffun6f  5176  dffun4f  5179  dffun7  5190  funopab  5198  funcnv2  5223  funcnv  5224  funcnveq  5226  fun2cnv  5227  fun11  5230  fununi  5231  funcnvuni  5232  funimaexglem  5246  fnres  5279  fnopabg  5286  rexrnmpt  5603  dff13  5709  oprabidlem  5842  eqoprab2b  5869  mpo2eqb  5920  ralrnmpo  5925  dfer2  6470  pw1dc0el  6845  fiintim  6862  omniwomnimkv  7089  ltexprlemdisj  7505  recexprlemdisj  7529  isprm2  11965  bj-stal  13260  bj-nfalt  13276  bdceq  13355  bdcriota  13396  bj-axempty2  13407  bj-vprc  13409  bdinex1  13412  bj-zfpair2  13423  bj-uniex2  13429  bj-ssom  13449  bj-inf2vnlem2  13484  ss1oel2o  13504