Theorem albii 1493

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 1491	. 2 |- ( A. x ( ph <-> ps ) -> ( A. x ph <-> A. x ps ) )
2		albii.1	. 2 |- ( ph <-> ps )
3	1, 2	mpg 1474	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 1470  ax-gen 1472

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2albii  1494  hbxfrbi  1495  nfbii  1496  19.26-2  1505  19.26-3an  1506  alrot3  1508  alrot4  1509  albiim  1510  2albiim  1511  alnex  1522  nfalt  1601  aaanh  1609  aaan  1610  alinexa  1626  exintrbi  1656  19.21-2  1690  19.31r  1704  equsalh  1749  equsal  1750  equsalv  1816  sbcof2  1833  dvelimfALT2  1840  19.23vv  1907  sbanv  1913  pm11.53  1919  nfsbxy  1970  nfsbxyt  1971  sbcomxyyz  2000  sb9  2007  sbnf2  2009  2sb6  2012  sbcom2v  2013  sb6a  2016  2sb6rf  2018  sbalyz  2027  sbal  2028  sbal1yz  2029  sbal1  2030  sbalv  2033  2exsb  2037  nfsb4t  2042  dvelimf  2043  dveeq1  2047  sbal2  2048  sb8eu  2067  sb8euh  2077  eu1  2079  eu2  2098  mo3h  2107  moanim  2128  2eu4  2147  exists1  2150  eqcom  2207  hblem  2313  abeq2  2314  abeq1  2315  nfceqi  2344  abid2f  2374  dfrex2dc  2497  ralbii2  2516  r2alf  2523  nfraldya  2541  r3al  2550  r19.21t  2581  r19.23t  2613  rabid2  2683  rabbi  2684  ralv  2789  ceqsralt  2799  gencbval  2821  rspc2gv  2889  ralab  2933  ralrab2  2938  euind  2960  reu2  2961  reu3  2963  rmo4  2966  reu8  2969  rmo3f  2970  rmoim  2974  2reuswapdc  2977  reuind  2978  2rmorex  2979  ra5  3087  rmo2ilem  3088  rmo3  3090  ssalel  3181  ss2ab  3261  ss2rab  3269  rabss  3270  uniiunlem  3282  dfdif3  3283  ddifstab  3305  ssequn1  3343  unss  3347  ralunb  3354  ssin  3395  ssddif  3407  n0rf  3473  eq0  3479  eqv  3480  rabeq0  3490  abeq0  3491  disj  3509  disj3  3513  pwss  3632  ralsnsg  3670  ralsns  3671  disjsn  3695  euabsn2  3702  snssOLD  3759  snssb  3766  snsssn  3802  dfnfc2  3868  uni0b  3875  unissb  3880  elintrab  3897  ssintrab  3908  intun  3916  intpr  3917  dfiin2g  3960  iunss  3968  dfdisj2  4023  cbvdisj  4031  disjnim  4035  dftr2  4144  dftr5  4145  trint  4157  zfnuleu  4168  vnex  4175  inex1  4178  repizf2lem  4205  axpweq  4215  zfpow  4219  axpow2  4220  axpow3  4221  exmid01  4242  zfpair2  4254  ssextss  4264  frirrg  4397  sucel  4457  zfun  4481  uniex2  4483  setindel  4586  setind  4587  elirr  4589  en2lp  4602  zfregfr  4622  tfi  4630  peano5  4646  ssrel  4763  ssrel2  4765  eqrelrel  4776  reliun  4796  raliunxp  4819  relop  4828  dmopab3  4891  dm0rn0  4895  reldm0  4896  cotr  5064  issref  5065  asymref  5068  intirr  5069  sb8iota  5239  dffun2  5281  dffun4  5282  dffun6f  5284  dffun4f  5287  dffun7  5298  funopab  5306  funcnv2  5334  funcnv  5335  funcnveq  5337  fun2cnv  5338  fun11  5341  fununi  5342  funcnvuni  5343  funimaexglem  5357  fnres  5392  fnopabg  5399  rexrnmpt  5723  dff13  5837  iotaexel  5904  oprabidlem  5975  eqoprab2b  6003  mpo2eqb  6055  ralrnmpo  6060  dfer2  6621  pw1dc0el  7008  fiintim  7028  omniwomnimkv  7269  ltexprlemdisj  7719  recexprlemdisj  7743  nnwosdc  12360  isprm2  12439  ivthdich  15125  bj-stal  15685  bj-nfalt  15700  bdceq  15778  bdcriota  15819  bj-axempty2  15830  bj-vprc  15832  bdinex1  15835  bj-zfpair2  15846  bj-uniex2  15852  bj-ssom  15872  bj-inf2vnlem2  15907  ss1oel2o  15928