Theorem albii 1458

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

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

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 1435  ax-gen 1437

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  2albii  1459  hbxfrbi  1460  nfbii  1461  19.26-2  1470  19.26-3an  1471  alrot3  1473  alrot4  1474  albiim  1475  2albiim  1476  alnex  1487  nfalt  1566  aaanh  1574  aaan  1575  alinexa  1591  exintrbi  1621  19.21-2  1655  19.31r  1669  equsalh  1714  equsal  1715  equsalv  1781  sbcof2  1798  dvelimfALT2  1805  19.23vv  1872  sbanv  1877  pm11.53  1883  nfsbxy  1930  nfsbxyt  1931  sbcomxyyz  1960  sb9  1967  sbnf2  1969  2sb6  1972  sbcom2v  1973  sb6a  1976  2sb6rf  1978  sbalyz  1987  sbal  1988  sbal1yz  1989  sbal1  1990  sbalv  1993  2exsb  1997  nfsb4t  2002  dvelimf  2003  dveeq1  2007  sbal2  2008  sb8eu  2027  sb8euh  2037  eu1  2039  eu2  2058  mo3h  2067  moanim  2088  2eu4  2107  exists1  2110  eqcom  2167  hblem  2274  abeq2  2275  abeq1  2276  nfceqi  2304  abid2f  2334  dfrex2dc  2457  ralbii2  2476  r2alf  2483  nfraldya  2501  r3al  2510  r19.21t  2541  r19.23t  2573  rabid2  2642  rabbi  2643  ralv  2743  ceqsralt  2753  gencbval  2774  rspc2gv  2842  ralab  2886  ralrab2  2891  euind  2913  reu2  2914  reu3  2916  rmo4  2919  reu8  2922  rmo3f  2923  rmoim  2927  2reuswapdc  2930  reuind  2931  2rmorex  2932  ra5  3039  rmo2ilem  3040  rmo3  3042  dfss2  3131  ss2ab  3210  ss2rab  3218  rabss  3219  uniiunlem  3231  dfdif3  3232  ddifstab  3254  ssequn1  3292  unss  3296  ralunb  3303  ssin  3344  ssddif  3356  n0rf  3421  eq0  3427  eqv  3428  rabeq0  3438  abeq0  3439  disj  3457  disj3  3461  rgenm  3511  pwss  3575  ralsnsg  3613  ralsns  3614  disjsn  3638  euabsn2  3645  snss  3702  snsssn  3741  dfnfc2  3807  uni0b  3814  unissb  3819  elintrab  3836  ssintrab  3847  intun  3855  intpr  3856  dfiin2g  3899  iunss  3907  dfdisj2  3961  cbvdisj  3969  disjnim  3973  dftr2  4082  dftr5  4083  trint  4095  zfnuleu  4106  vnex  4113  inex1  4116  repizf2lem  4140  axpweq  4150  zfpow  4154  axpow2  4155  axpow3  4156  exmid01  4177  zfpair2  4188  ssextss  4198  frirrg  4328  sucel  4388  zfun  4412  uniex2  4414  setindel  4515  setind  4516  elirr  4518  en2lp  4531  zfregfr  4551  tfi  4559  peano5  4575  ssrel  4692  ssrel2  4694  eqrelrel  4705  reliun  4725  raliunxp  4745  relop  4754  dmopab3  4817  dm0rn0  4821  reldm0  4822  cotr  4985  issref  4986  asymref  4989  intirr  4990  sb8iota  5160  dffun2  5198  dffun4  5199  dffun6f  5201  dffun4f  5204  dffun7  5215  funopab  5223  funcnv2  5248  funcnv  5249  funcnveq  5251  fun2cnv  5252  fun11  5255  fununi  5256  funcnvuni  5257  funimaexglem  5271  fnres  5304  fnopabg  5311  rexrnmpt  5628  dff13  5736  oprabidlem  5873  eqoprab2b  5900  mpo2eqb  5951  ralrnmpo  5956  dfer2  6502  pw1dc0el  6877  fiintim  6894  omniwomnimkv  7131  ltexprlemdisj  7547  recexprlemdisj  7571  nnwosdc  11972  isprm2  12049  bj-stal  13630  bj-nfalt  13645  bdceq  13724  bdcriota  13765  bj-axempty2  13776  bj-vprc  13778  bdinex1  13781  bj-zfpair2  13792  bj-uniex2  13798  bj-ssom  13818  bj-inf2vnlem2  13853  ss1oel2o  13873