Theorem albii 1481

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 1479	. 2 |- ( A. x ( ph <-> ps ) -> ( A. x ph <-> A. x ps ) )
2		albii.1	. 2 |- ( ph <-> ps )
3	1, 2	mpg 1462	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 1458  ax-gen 1460

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2albii  1482  hbxfrbi  1483  nfbii  1484  19.26-2  1493  19.26-3an  1494  alrot3  1496  alrot4  1497  albiim  1498  2albiim  1499  alnex  1510  nfalt  1589  aaanh  1597  aaan  1598  alinexa  1614  exintrbi  1644  19.21-2  1678  19.31r  1692  equsalh  1737  equsal  1738  equsalv  1804  sbcof2  1821  dvelimfALT2  1828  19.23vv  1895  sbanv  1901  pm11.53  1907  nfsbxy  1958  nfsbxyt  1959  sbcomxyyz  1988  sb9  1995  sbnf2  1997  2sb6  2000  sbcom2v  2001  sb6a  2004  2sb6rf  2006  sbalyz  2015  sbal  2016  sbal1yz  2017  sbal1  2018  sbalv  2021  2exsb  2025  nfsb4t  2030  dvelimf  2031  dveeq1  2035  sbal2  2036  sb8eu  2055  sb8euh  2065  eu1  2067  eu2  2086  mo3h  2095  moanim  2116  2eu4  2135  exists1  2138  eqcom  2195  hblem  2301  abeq2  2302  abeq1  2303  nfceqi  2332  abid2f  2362  dfrex2dc  2485  ralbii2  2504  r2alf  2511  nfraldya  2529  r3al  2538  r19.21t  2569  r19.23t  2601  rabid2  2671  rabbi  2672  ralv  2777  ceqsralt  2787  gencbval  2809  rspc2gv  2877  ralab  2921  ralrab2  2926  euind  2948  reu2  2949  reu3  2951  rmo4  2954  reu8  2957  rmo3f  2958  rmoim  2962  2reuswapdc  2965  reuind  2966  2rmorex  2967  ra5  3075  rmo2ilem  3076  rmo3  3078  dfss2  3169  ss2ab  3248  ss2rab  3256  rabss  3257  uniiunlem  3269  dfdif3  3270  ddifstab  3292  ssequn1  3330  unss  3334  ralunb  3341  ssin  3382  ssddif  3394  n0rf  3460  eq0  3466  eqv  3467  rabeq0  3477  abeq0  3478  disj  3496  disj3  3500  pwss  3618  ralsnsg  3656  ralsns  3657  disjsn  3681  euabsn2  3688  snssOLD  3745  snssb  3752  snsssn  3788  dfnfc2  3854  uni0b  3861  unissb  3866  elintrab  3883  ssintrab  3894  intun  3902  intpr  3903  dfiin2g  3946  iunss  3954  dfdisj2  4009  cbvdisj  4017  disjnim  4021  dftr2  4130  dftr5  4131  trint  4143  zfnuleu  4154  vnex  4161  inex1  4164  repizf2lem  4191  axpweq  4201  zfpow  4205  axpow2  4206  axpow3  4207  exmid01  4228  zfpair2  4240  ssextss  4250  frirrg  4382  sucel  4442  zfun  4466  uniex2  4468  setindel  4571  setind  4572  elirr  4574  en2lp  4587  zfregfr  4607  tfi  4615  peano5  4631  ssrel  4748  ssrel2  4750  eqrelrel  4761  reliun  4781  raliunxp  4804  relop  4813  dmopab3  4876  dm0rn0  4880  reldm0  4881  cotr  5048  issref  5049  asymref  5052  intirr  5053  sb8iota  5223  dffun2  5265  dffun4  5266  dffun6f  5268  dffun4f  5271  dffun7  5282  funopab  5290  funcnv2  5315  funcnv  5316  funcnveq  5318  fun2cnv  5319  fun11  5322  fununi  5323  funcnvuni  5324  funimaexglem  5338  fnres  5371  fnopabg  5378  rexrnmpt  5702  dff13  5812  iotaexel  5879  oprabidlem  5950  eqoprab2b  5977  mpo2eqb  6029  ralrnmpo  6034  dfer2  6590  pw1dc0el  6969  fiintim  6987  omniwomnimkv  7228  ltexprlemdisj  7668  recexprlemdisj  7692  nnwosdc  12179  isprm2  12258  ivthdich  14832  bj-stal  15311  bj-nfalt  15326  bdceq  15404  bdcriota  15445  bj-axempty2  15456  bj-vprc  15458  bdinex1  15461  bj-zfpair2  15472  bj-uniex2  15478  bj-ssom  15498  bj-inf2vnlem2  15533  ss1oel2o  15554