Theorem albii 1747

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

Syntax hints:   <-> wb 196   A.wal 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  2albii  1748  hbxfrbi  1752  alex  1753  2nalexn  1755  2exnaln  1756  imnang  1769  alexn  1771  nfnbi  1781  19.26-2  1799  19.26-3an  1800  19.43OLD  1811  albiim  1816  2albiim  1817  nfbiiOLD  1836  19.32v  1869  19.31v  1870  19.23vv  1903  pm11.53v  1906  19.12vvv  1907  equsalvw  1931  alrot3  2038  alrot4  2039  19.21-2  2078  19.23t  2079  19.32  2101  19.31  2102  equsalv  2108  equsalhw  2123  aaan  2170  pm11.53  2179  19.12vv  2180  19.21-2OLD  2215  19.23tOLD  2218  equsal  2291  sbcom3  2411  2sb6  2444  2sb6rf  2452  sbex  2463  sbalv  2464  sb8eu  2503  eu1  2510  2mo2  2550  2eu1  2553  2eu3  2555  exists1  2561  hblem  2731  abeq2  2732  abeq1  2733  abbi  2737  abeq2f  2792  r2allem  2937  r3al  2940  r19.21t  2955  r19.21v  2960  ralbii2  2978  r19.23t  3021  rabid2  3118  rabid2f  3119  rabbi  3120  eqvf  3204  abv  3206  ralv  3219  ceqsralt  3229  rspc2gv  3321  ralxpxfr2d  3327  ralab  3367  ralrab2  3372  euind  3393  reu2  3394  reu3  3396  rmo4  3399  reu8  3402  rmoim  3407  2reuswap  3410  reuind  3411  2reu5lem2  3414  2reu5lem3  3415  rmo2  3526  rmo3  3528  dfss2  3591  ss2ab  3670  ss2rab  3678  rabss  3679  uniiunlem  3691  ssequn1  3783  unss  3787  ralunb  3794  ssin  3835  eq0f  3925  n0fOLD  3928  ssdif0  3942  inssdif0  3947  ab0  3951  disj  4017  disj3  4021  ssundif  4052  ralf0  4078  pwss  4175  rabsssn  4215  ralsnsg  4216  disjsn  4246  euabsn2  4260  snss  4316  pwpw0  4344  pwsnALT  4429  dfnfc2  4454  dfnfc2OLD  4455  unissb  4469  elintrab  4488  ssintrab  4500  intun  4509  intpr  4510  dfiin2g  4553  iunss  4561  dfdisj2  4622  cbvdisj  4630  disjor  4634  dftr2  4754  dftr5  4755  trint  4768  axrep1  4772  axrep5  4776  axsep  4780  zfnuleu  4786  axnulALT  4787  vprc  4796  inex1  4799  axpweq  4842  zfpow  4844  axpow2  4845  axpow3  4846  reusv2lem4  4872  nfnid  4897  dtruALT  4899  zfpair2  4907  dtruALT2  4911  ssextss  4922  moabex  4927  dffr2  5079  dfepfr  5099  frinxp  5184  ssrelOLD  5208  ssrel2  5210  eqrelrel  5221  reliun  5239  raliunxp  5261  relop  5272  dmopab3  5337  dm0rn0  5342  reldm0  5343  dffr3  5498  cotrg  5507  issref  5509  asymref  5512  asymref2  5513  intirr  5514  dffr4  5696  sucel  5798  sb8iota  5858  dffun2  5898  dffun3  5899  dffun4  5900  dffun5  5901  dffun6f  5902  dffun7  5915  funopab  5923  funcnv2  5957  funcnv  5958  fun2cnv  5960  fun11  5963  fununi  5964  fnres  6007  mptfnf  6015  fnopabg  6017  brprcneu  6184  dffv2  6271  fvn0ssdmfun  6350  dff13  6512  eqoprab2b  6713  mpt22eqb  6769  ralrnmpt2  6775  zfun  6950  uniex2  6952  funcnvuni  7119  dfer2  7743  fiint  8237  marypha1lem  8339  marypha2lem3  8343  inf2  8520  axinf2  8537  scottexs  8750  scott0s  8751  aceq1  8940  dfac4  8945  dfac7  8954  dfac0  8955  dfac1  8956  dfac10  8959  dfac10c  8960  dfac10b  8961  kmlem4  8975  kmlem12  8983  kmlem14  8985  kmlem15  8986  kmlem16  8987  dfackm  8988  ac6n  9307  axpowndlem3  9421  zfcndrep  9436  zfcndun  9437  zfcndpow  9438  axgroth5  9646  axgroth2  9647  grothpw  9648  axgroth4  9654  grothprim  9656  sstskm  9664  fimaxre3  10970  infm3  10982  nnwos  11755  cotr2g  13715  brtrclfv  13743  trclfvcotr  13750  rpnnen2lem12  14954  isprm2  15395  vdwmc2  15683  pgpfac1  18479  pgpfac  18483  iunocv  20025  2ndcdisj2  21260  hausdiag  21448  rnelfmlem  21756  alexsubALTlem3  21853  cnextfun  21868  itg2leub  23501  mptelee  25775  nmoubi  27627  nmobndseqi  27634  nmobndseqiALT  27635  isch2  28080  isch3  28098  choc0  28185  nmopub  28767  nmfnleub  28784  xfree2  29304  moel  29323  mo5f  29324  nmo  29325  2reuswap2  29328  rmo3f  29335  rmo4fOLD  29336  rabeqsnd  29342  cbvdisjf  29385  disjorf  29392  ssrelf  29425  funcnvmptOLD  29467  funcnvmpt  29468  funcnv5mpt  29469  ballotlem2  30550  bnj89  30787  bnj115  30791  bnj145OLD  30795  bnj538OLD  30810  bnj1143  30861  bnj110  30928  bnj611  30988  bnj864  30992  bnj865  30993  bnj1000  31011  bnj978  31019  bnj1049  31042  bnj1052  31043  bnj1090  31047  bnj1030  31055  bnj1133  31057  bnj1171  31068  bnj1172  31069  bnj1174  31071  bnj1176  31073  bnj1204  31080  bnj1253  31085  bnj1388  31101  bnj1523  31139  axrepprim  31579  axunprim  31580  axpowprim  31581  axinfprim  31583  axacprim  31584  untuni  31586  dffr5  31643  elintfv  31662  dfon2lem8  31695  dfon2lem9  31696  19.12b  31707  brtxpsd3  32003  dfom5b  32019  dffun10  32021  bj-notalbii  32598  bj-ssbeq  32627  bj-ssb0  32628  bj-ssb1a  32632  bj-ssb1  32633  bj-ax12ssb  32635  bj-ssbn  32641  bj-ssbcom3lem  32650  bj-hbext  32701  bj-nfalt  32702  bj-abeq2  32773  bj-abeq1  32774  bj-axrep1  32788  bj-axrep5  32792  bj-axsep  32793  bj-zfpow  32795  ax11-pm2  32823  bj-sbnf  32828  bj-hblem  32849  bj-ralvw  32865  bj-ralcom4  32868  bj-sbeq  32896  bj-nfcf  32920  bj-snsetex  32951  bj-raldifsn  33054  wl-equsalcom  33328  wl-sb8et  33334  wl-2sb6d  33341  wl-alanbii  33351  wl-sb8eut  33359  wl-sbcom3  33372  poimirlem25  33434  poimirlem30  33439  heibor1lem  33608  sbcalfi  33919  mpt2bi123f  33971  mptbi12f  33975  ralanid  34010  3albii  34012  ineccnvmo  34122  alrmomo  34123  dvelimf-o  34214  axc11n-16  34223  pmapglbx  35055  dford4  37596  rp-fakeinunass  37861  rababg  37879  elmapintrab  37882  elinintrab  37883  undmrnresiss  37910  clss2lem  37918  cotrintab  37921  elintima  37945  ss2iundf  37951  relexp0eq  37993  dfhe3  38069  snhesn  38080  psshepw  38082  dffrege76  38233  frege77  38234  frege110  38267  dffrege115  38272  frege116  38273  frege118  38275  frege131  38288  ntrneikb  38392  ntrneixb  38393  pm10.541  38566  pm10.542  38567  19.21vv  38575  19.31vv  38583  19.28vv  38585  pm11.62  38594  axc11next  38607  pm13.196a  38615  2sbc6g  38616  elnev  38639  conss34OLD  38646  hbexgVD  39142  iunssf  39263  rabssf  39302  2rexsb  41170  2rmoswap  41184  spr0nelg  41726  dffun3f  42429  setrec1lem2  42435  setrec2  42442  alimp-surprise  42526  alimp-no-surprise  42527