Theorem albii 1470

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

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

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 1447  ax-gen 1449

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2albii  1471  hbxfrbi  1472  nfbii  1473  19.26-2  1482  19.26-3an  1483  alrot3  1485  alrot4  1486  albiim  1487  2albiim  1488  alnex  1499  nfalt  1578  aaanh  1586  aaan  1587  alinexa  1603  exintrbi  1633  19.21-2  1667  19.31r  1681  equsalh  1726  equsal  1727  equsalv  1793  sbcof2  1810  dvelimfALT2  1817  19.23vv  1884  sbanv  1889  pm11.53  1895  nfsbxy  1942  nfsbxyt  1943  sbcomxyyz  1972  sb9  1979  sbnf2  1981  2sb6  1984  sbcom2v  1985  sb6a  1988  2sb6rf  1990  sbalyz  1999  sbal  2000  sbal1yz  2001  sbal1  2002  sbalv  2005  2exsb  2009  nfsb4t  2014  dvelimf  2015  dveeq1  2019  sbal2  2020  sb8eu  2039  sb8euh  2049  eu1  2051  eu2  2070  mo3h  2079  moanim  2100  2eu4  2119  exists1  2122  eqcom  2179  hblem  2285  abeq2  2286  abeq1  2287  nfceqi  2315  abid2f  2345  dfrex2dc  2468  ralbii2  2487  r2alf  2494  nfraldya  2512  r3al  2521  r19.21t  2552  r19.23t  2584  rabid2  2654  rabbi  2655  ralv  2755  ceqsralt  2765  gencbval  2786  rspc2gv  2854  ralab  2898  ralrab2  2903  euind  2925  reu2  2926  reu3  2928  rmo4  2931  reu8  2934  rmo3f  2935  rmoim  2939  2reuswapdc  2942  reuind  2943  2rmorex  2944  ra5  3052  rmo2ilem  3053  rmo3  3055  dfss2  3145  ss2ab  3224  ss2rab  3232  rabss  3233  uniiunlem  3245  dfdif3  3246  ddifstab  3268  ssequn1  3306  unss  3310  ralunb  3317  ssin  3358  ssddif  3370  n0rf  3436  eq0  3442  eqv  3443  rabeq0  3453  abeq0  3454  disj  3472  disj3  3476  rgenm  3526  pwss  3592  ralsnsg  3630  ralsns  3631  disjsn  3655  euabsn2  3662  snssOLD  3719  snssb  3726  snsssn  3762  dfnfc2  3828  uni0b  3835  unissb  3840  elintrab  3857  ssintrab  3868  intun  3876  intpr  3877  dfiin2g  3920  iunss  3928  dfdisj2  3983  cbvdisj  3991  disjnim  3995  dftr2  4104  dftr5  4105  trint  4117  zfnuleu  4128  vnex  4135  inex1  4138  repizf2lem  4162  axpweq  4172  zfpow  4176  axpow2  4177  axpow3  4178  exmid01  4199  zfpair2  4211  ssextss  4221  frirrg  4351  sucel  4411  zfun  4435  uniex2  4437  setindel  4538  setind  4539  elirr  4541  en2lp  4554  zfregfr  4574  tfi  4582  peano5  4598  ssrel  4715  ssrel2  4717  eqrelrel  4728  reliun  4748  raliunxp  4769  relop  4778  dmopab3  4841  dm0rn0  4845  reldm0  4846  cotr  5011  issref  5012  asymref  5015  intirr  5016  sb8iota  5186  dffun2  5227  dffun4  5228  dffun6f  5230  dffun4f  5233  dffun7  5244  funopab  5252  funcnv2  5277  funcnv  5278  funcnveq  5280  fun2cnv  5281  fun11  5284  fununi  5285  funcnvuni  5286  funimaexglem  5300  fnres  5333  fnopabg  5340  rexrnmpt  5660  dff13  5769  oprabidlem  5906  eqoprab2b  5933  mpo2eqb  5984  ralrnmpo  5989  dfer2  6536  pw1dc0el  6911  fiintim  6928  omniwomnimkv  7165  ltexprlemdisj  7605  recexprlemdisj  7629  nnwosdc  12040  isprm2  12117  bj-stal  14504  bj-nfalt  14519  bdceq  14597  bdcriota  14638  bj-axempty2  14649  bj-vprc  14651  bdinex1  14654  bj-zfpair2  14665  bj-uniex2  14671  bj-ssom  14691  bj-inf2vnlem2  14726  ss1oel2o  14746