Theorem albii 1516

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

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

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 1493  ax-gen 1495

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  2albii  1517  hbxfrbi  1518  nfbii  1519  19.26-2  1528  19.26-3an  1529  alrot3  1531  alrot4  1532  albiim  1533  2albiim  1534  alnex  1545  nfalt  1624  aaanh  1632  aaan  1633  alinexa  1649  exintrbi  1679  19.21-2  1713  19.31r  1727  equsalh  1772  equsal  1773  equsalv  1839  sbcof2  1856  dvelimfALT2  1863  19.23vv  1930  sbanv  1936  pm11.53  1942  nfsbxy  1993  nfsbxyt  1994  sbcomxyyz  2023  sb9  2030  sbnf2  2032  2sb6  2035  sbcom2v  2036  sb6a  2039  2sb6rf  2041  sbalyz  2050  sbal  2051  sbal1yz  2052  sbal1  2053  sbalv  2056  2exsb  2060  nfsb4t  2065  dvelimf  2066  dveeq1  2070  sbal2  2071  sb8eu  2090  sb8euh  2100  eu1  2102  eu2  2122  mo3h  2131  moanim  2152  2eu4  2171  exists1  2174  eqcom  2231  hblem  2337  abeq2  2338  abeq1  2339  nfceqi  2368  abid2f  2398  dfrex2dc  2521  ralbii2  2540  r2alf  2547  nfraldya  2565  r3al  2574  r19.21t  2605  r19.23t  2638  rabid2  2708  rabbi  2709  ralv  2818  ceqsralt  2828  gencbval  2850  rspc2gv  2920  ralab  2964  ralrab2  2969  euind  2991  reu2  2992  reu3  2994  rmo4  2997  reu8  3000  rmo3f  3001  rmoim  3005  2reuswapdc  3008  reuind  3009  2rmorex  3010  ra5  3119  rmo2ilem  3120  rmo3  3122  ssalel  3213  ss2ab  3293  ss2rab  3301  rabss  3302  uniiunlem  3314  dfdif3  3315  ddifstab  3337  ssequn1  3375  unss  3379  ralunb  3386  ssin  3427  ssddif  3439  n0rf  3505  eq0  3511  eqv  3512  rabeq0  3522  abeq0  3523  disj  3541  disj3  3545  pwss  3666  ralsnsg  3704  ralsns  3705  disjsn  3729  euabsn2  3738  snssOLD  3797  snssb  3804  snsssn  3842  dfnfc2  3909  uni0b  3916  unissb  3921  elintrab  3938  ssintrab  3949  intun  3957  intpr  3958  dfiin2g  4001  iunss  4009  dfdisj2  4064  cbvdisj  4072  disjnim  4076  dftr2  4187  dftr5  4188  trint  4200  zfnuleu  4211  vnex  4218  inex1  4221  repizf2lem  4249  axpweq  4259  zfpow  4263  axpow2  4264  axpow3  4265  exmid01  4286  zfpair2  4298  ssextss  4310  frirrg  4445  sucel  4505  zfun  4529  uniex2  4531  setindel  4634  setind  4635  elirr  4637  en2lp  4650  zfregfr  4670  tfi  4678  peano5  4694  ssrel  4812  ssrel2  4814  eqrelrel  4825  reliun  4846  raliunxp  4869  relop  4878  dmopab3  4942  dm0rn0  4946  reldm0  4947  cotr  5116  issref  5117  asymref  5120  intirr  5121  sb8iota  5292  dffun2  5334  dffun4  5335  dffun6f  5337  dffun4f  5340  dffun7  5351  funopab  5359  funcnv2  5387  funcnv  5388  funcnveq  5390  fun2cnv  5391  fun11  5394  fununi  5395  funcnvuni  5396  funimaexglem  5410  fnres  5446  fnopabg  5453  rexrnmpt  5786  dff13  5904  iotaexel  5971  oprabidlem  6044  eqoprab2b  6074  mpo2eqb  6126  ralrnmpo  6131  dfer2  6698  pw1dc0el  7096  fiintim  7116  omniwomnimkv  7357  ltexprlemdisj  7816  recexprlemdisj  7840  nnwosdc  12600  isprm2  12679  ivthdich  15367  bj-stal  16281  bj-nfalt  16296  bdceq  16373  bdcriota  16414  bj-axempty2  16425  bj-vprc  16427  bdinex1  16430  bj-zfpair2  16441  bj-uniex2  16447  bj-ssom  16467  bj-inf2vnlem2  16502  ss1oel2o  16522