Theorem albii 1484

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 1482	. 2 |- ( A. x ( ph <-> ps ) -> ( A. x ph <-> A. x ps ) )
2		albii.1	. 2 |- ( ph <-> ps )
3	1, 2	mpg 1465	1 |- ( A. x ph <-> A. x ps )

Syntax hints:   <-> wb 105   A.wal 1362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2albii  1485  hbxfrbi  1486  nfbii  1487  19.26-2  1496  19.26-3an  1497  alrot3  1499  alrot4  1500  albiim  1501  2albiim  1502  alnex  1513  nfalt  1592  aaanh  1600  aaan  1601  alinexa  1617  exintrbi  1647  19.21-2  1681  19.31r  1695  equsalh  1740  equsal  1741  equsalv  1807  sbcof2  1824  dvelimfALT2  1831  19.23vv  1898  sbanv  1904  pm11.53  1910  nfsbxy  1961  nfsbxyt  1962  sbcomxyyz  1991  sb9  1998  sbnf2  2000  2sb6  2003  sbcom2v  2004  sb6a  2007  2sb6rf  2009  sbalyz  2018  sbal  2019  sbal1yz  2020  sbal1  2021  sbalv  2024  2exsb  2028  nfsb4t  2033  dvelimf  2034  dveeq1  2038  sbal2  2039  sb8eu  2058  sb8euh  2068  eu1  2070  eu2  2089  mo3h  2098  moanim  2119  2eu4  2138  exists1  2141  eqcom  2198  hblem  2304  abeq2  2305  abeq1  2306  nfceqi  2335  abid2f  2365  dfrex2dc  2488  ralbii2  2507  r2alf  2514  nfraldya  2532  r3al  2541  r19.21t  2572  r19.23t  2604  rabid2  2674  rabbi  2675  ralv  2780  ceqsralt  2790  gencbval  2812  rspc2gv  2880  ralab  2924  ralrab2  2929  euind  2951  reu2  2952  reu3  2954  rmo4  2957  reu8  2960  rmo3f  2961  rmoim  2965  2reuswapdc  2968  reuind  2969  2rmorex  2970  ra5  3078  rmo2ilem  3079  rmo3  3081  dfss2  3172  ss2ab  3251  ss2rab  3259  rabss  3260  uniiunlem  3272  dfdif3  3273  ddifstab  3295  ssequn1  3333  unss  3337  ralunb  3344  ssin  3385  ssddif  3397  n0rf  3463  eq0  3469  eqv  3470  rabeq0  3480  abeq0  3481  disj  3499  disj3  3503  pwss  3621  ralsnsg  3659  ralsns  3660  disjsn  3684  euabsn2  3691  snssOLD  3748  snssb  3755  snsssn  3791  dfnfc2  3857  uni0b  3864  unissb  3869  elintrab  3886  ssintrab  3897  intun  3905  intpr  3906  dfiin2g  3949  iunss  3957  dfdisj2  4012  cbvdisj  4020  disjnim  4024  dftr2  4133  dftr5  4134  trint  4146  zfnuleu  4157  vnex  4164  inex1  4167  repizf2lem  4194  axpweq  4204  zfpow  4208  axpow2  4209  axpow3  4210  exmid01  4231  zfpair2  4243  ssextss  4253  frirrg  4385  sucel  4445  zfun  4469  uniex2  4471  setindel  4574  setind  4575  elirr  4577  en2lp  4590  zfregfr  4610  tfi  4618  peano5  4634  ssrel  4751  ssrel2  4753  eqrelrel  4764  reliun  4784  raliunxp  4807  relop  4816  dmopab3  4879  dm0rn0  4883  reldm0  4884  cotr  5051  issref  5052  asymref  5055  intirr  5056  sb8iota  5226  dffun2  5268  dffun4  5269  dffun6f  5271  dffun4f  5274  dffun7  5285  funopab  5293  funcnv2  5318  funcnv  5319  funcnveq  5321  fun2cnv  5322  fun11  5325  fununi  5326  funcnvuni  5327  funimaexglem  5341  fnres  5374  fnopabg  5381  rexrnmpt  5705  dff13  5815  iotaexel  5882  oprabidlem  5953  eqoprab2b  5980  mpo2eqb  6032  ralrnmpo  6037  dfer2  6593  pw1dc0el  6972  fiintim  6992  omniwomnimkv  7233  ltexprlemdisj  7673  recexprlemdisj  7697  nnwosdc  12206  isprm2  12285  ivthdich  14889  bj-stal  15395  bj-nfalt  15410  bdceq  15488  bdcriota  15529  bj-axempty2  15540  bj-vprc  15542  bdinex1  15545  bj-zfpair2  15556  bj-uniex2  15562  bj-ssom  15582  bj-inf2vnlem2  15617  ss1oel2o  15638