Theorem albii 1494

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

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

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 1471  ax-gen 1473

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2albii  1495  hbxfrbi  1496  nfbii  1497  19.26-2  1506  19.26-3an  1507  alrot3  1509  alrot4  1510  albiim  1511  2albiim  1512  alnex  1523  nfalt  1602  aaanh  1610  aaan  1611  alinexa  1627  exintrbi  1657  19.21-2  1691  19.31r  1705  equsalh  1750  equsal  1751  equsalv  1817  sbcof2  1834  dvelimfALT2  1841  19.23vv  1908  sbanv  1914  pm11.53  1920  nfsbxy  1971  nfsbxyt  1972  sbcomxyyz  2001  sb9  2008  sbnf2  2010  2sb6  2013  sbcom2v  2014  sb6a  2017  2sb6rf  2019  sbalyz  2028  sbal  2029  sbal1yz  2030  sbal1  2031  sbalv  2034  2exsb  2038  nfsb4t  2043  dvelimf  2044  dveeq1  2048  sbal2  2049  sb8eu  2068  sb8euh  2078  eu1  2080  eu2  2100  mo3h  2109  moanim  2130  2eu4  2149  exists1  2152  eqcom  2209  hblem  2315  abeq2  2316  abeq1  2317  nfceqi  2346  abid2f  2376  dfrex2dc  2499  ralbii2  2518  r2alf  2525  nfraldya  2543  r3al  2552  r19.21t  2583  r19.23t  2615  rabid2  2685  rabbi  2686  ralv  2794  ceqsralt  2804  gencbval  2826  rspc2gv  2896  ralab  2940  ralrab2  2945  euind  2967  reu2  2968  reu3  2970  rmo4  2973  reu8  2976  rmo3f  2977  rmoim  2981  2reuswapdc  2984  reuind  2985  2rmorex  2986  ra5  3095  rmo2ilem  3096  rmo3  3098  ssalel  3189  ss2ab  3269  ss2rab  3277  rabss  3278  uniiunlem  3290  dfdif3  3291  ddifstab  3313  ssequn1  3351  unss  3355  ralunb  3362  ssin  3403  ssddif  3415  n0rf  3481  eq0  3487  eqv  3488  rabeq0  3498  abeq0  3499  disj  3517  disj3  3521  pwss  3642  ralsnsg  3680  ralsns  3681  disjsn  3705  euabsn2  3712  snssOLD  3770  snssb  3777  snsssn  3815  dfnfc2  3882  uni0b  3889  unissb  3894  elintrab  3911  ssintrab  3922  intun  3930  intpr  3931  dfiin2g  3974  iunss  3982  dfdisj2  4037  cbvdisj  4045  disjnim  4049  dftr2  4160  dftr5  4161  trint  4173  zfnuleu  4184  vnex  4191  inex1  4194  repizf2lem  4221  axpweq  4231  zfpow  4235  axpow2  4236  axpow3  4237  exmid01  4258  zfpair2  4270  ssextss  4282  frirrg  4415  sucel  4475  zfun  4499  uniex2  4501  setindel  4604  setind  4605  elirr  4607  en2lp  4620  zfregfr  4640  tfi  4648  peano5  4664  ssrel  4781  ssrel2  4783  eqrelrel  4794  reliun  4814  raliunxp  4837  relop  4846  dmopab3  4910  dm0rn0  4914  reldm0  4915  cotr  5083  issref  5084  asymref  5087  intirr  5088  sb8iota  5258  dffun2  5300  dffun4  5301  dffun6f  5303  dffun4f  5306  dffun7  5317  funopab  5325  funcnv2  5353  funcnv  5354  funcnveq  5356  fun2cnv  5357  fun11  5360  fununi  5361  funcnvuni  5362  funimaexglem  5376  fnres  5412  fnopabg  5419  rexrnmpt  5746  dff13  5860  iotaexel  5927  oprabidlem  5998  eqoprab2b  6026  mpo2eqb  6078  ralrnmpo  6083  dfer2  6644  pw1dc0el  7034  fiintim  7054  omniwomnimkv  7295  ltexprlemdisj  7754  recexprlemdisj  7778  nnwosdc  12475  isprm2  12554  ivthdich  15240  bj-stal  15885  bj-nfalt  15900  bdceq  15977  bdcriota  16018  bj-axempty2  16029  bj-vprc  16031  bdinex1  16034  bj-zfpair2  16045  bj-uniex2  16051  bj-ssom  16071  bj-inf2vnlem2  16106  ss1oel2o  16127