Theorem albii 1359

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

Syntax hints:   <-> wb 98   A.wal 1241

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  2albii  1360  hbxfrbi  1361  nfbii  1362  19.26-2  1371  19.26-3an  1372  alrot3  1374  alrot4  1375  albiim  1376  2albiim  1377  alnex  1388  nfalt  1470  aaanh  1478  aaan  1479  alinexa  1494  exintrbi  1524  19.21-2  1557  19.31r  1571  equsalh  1614  equsal  1615  sbcof2  1691  dvelimfALT2  1698  19.23vv  1764  sbanv  1769  pm11.53  1775  nfsbxy  1818  nfsbxyt  1819  sbcomxyyz  1846  sb9  1855  sbnf2  1857  2sb6  1860  sbcom2v  1861  sb6a  1864  2sb6rf  1866  sbalyz  1875  sbal  1876  sbal1yz  1877  sbal1  1878  sbalv  1881  2exsb  1885  nfsb4t  1890  dvelimf  1891  dveeq1  1895  sbal2  1898  sb8eu  1913  sb8euh  1923  eu1  1925  eu2  1944  mo3h  1953  moanim  1974  2eu4  1993  exists1  1996  eqcom  2042  hblem  2145  abeq2  2146  abeq1  2147  nfceqi  2174  abid2f  2202  ralbii2  2334  r2alf  2341  nfraldya  2358  r3al  2366  r19.21t  2394  r19.23t  2423  rabid2  2486  rabbi  2487  ralv  2571  ceqsralt  2581  gencbval  2602  ralab  2701  ralrab2  2706  euind  2728  reu2  2729  reu3  2731  rmo4  2734  reu8  2737  rmoim  2740  2reuswapdc  2743  reuind  2744  2rmorex  2745  ra5  2846  rmo2ilem  2847  rmo3  2849  dfss2  2934  ss2ab  3008  ss2rab  3016  rabss  3017  uniiunlem  3028  ssequn1  3113  unss  3117  ralunb  3124  ssin  3159  ssddif  3171  n0rf  3233  eq0  3239  eqv  3240  rabeq0  3247  abeq0  3248  disj  3268  disj3  3272  rgenm  3323  pwss  3374  ralsnsg  3407  ralsns  3408  disjsn  3432  euabsn2  3439  snss  3494  snsssn  3532  dfnfc2  3598  uni0b  3605  unissb  3610  elintrab  3627  ssintrab  3638  intun  3646  intpr  3647  dfiin2g  3690  iunss  3698  dfdisj2  3747  cbvdisj  3755  dftr2  3856  dftr5  3857  trint  3869  zfnuleu  3881  vprc  3888  inex1  3891  repizf2lem  3914  axpweq  3924  zfpow  3928  axpow2  3929  axpow3  3930  zfpair2  3945  ssextss  3956  frirrg  4087  sucel  4147  zfun  4171  uniex2  4173  setindel  4263  setind  4264  elirr  4266  en2lp  4278  zfregfr  4298  tfi  4305  peano5  4321  ssrel  4428  ssrel2  4430  eqrelrel  4441  reliun  4458  raliunxp  4477  relop  4486  dmopab3  4548  dm0rn0  4552  reldm0  4553  cotr  4706  issref  4707  asymref  4710  intirr  4711  sb8iota  4874  dffun2  4912  dffun4  4913  dffun6f  4915  dffun4f  4918  dffun7  4928  funopab  4935  funcnv2  4959  funcnv  4960  funcnveq  4962  fun2cnv  4963  fun11  4966  fununi  4967  funcnvuni  4968  funimaexglem  4982  fnres  5015  fnopabg  5022  rexrnmpt  5310  dff13  5407  oprabidlem  5536  eqoprab2b  5563  mpt22eqb  5610  ralrnmpt2  5615  dfer2  6107  ltexprlemdisj  6704  recexprlemdisj  6728  bj-nfalt  9904  bdceq  9962  bdcriota  10003  bj-axempty2  10014  bj-vprc  10016  bdinex1  10019  bj-zfpair2  10030  bj-uniex2  10036  bj-ssom  10060  peano5setOLD  10065  bj-inf2vnlem2  10096