Theorem simprbi 502

Description: Deduction eliminating a conjunct. (Contributed by NM, 27-May-1998.)

Hypothesis

Ref	Expression
simprbi.1	⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))

Assertion

Ref	Expression
simprbi	⊢ (𝜑 → 𝜒)

Proof of Theorem simprbi

Step	Hyp	Ref	Expression
1		simprbi.1	. . 3 ⊢ (𝜑 ↔ (𝜓 ∧ 𝜒))
2	1	biimpi 219	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simprd 500	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400

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

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  simplbiim  513  xornan  1547  eumo  2604  reurmo  3370  pssne  4052  pssn2lp  4058  ssnpss  4060  eldifn  4085  elinel2  4154  rabsnt  4696  eldifsni  4757  unimax  4909  ssintub  4930  moop2  5485  pwssun  5553  weso  5652  opelxp2  5704  predpo  6324  frpoinsg  6344  ordwe  6373  funmo  6552  funopg  6570  funun  6582  fununi  6611  funimaexg  6622  fndm  6638  frn  6713  f1ss  6781  f1ssr  6782  forn  6795  f1f1orn  6832  f1orescnv  6836  f1imacnv  6837  funcocnv2  6846  dffv2  6976  exfo  7100  foelrn  7102  foelrnf  7103  isorel  7324  isoini2  7337  f1ofveu  7404  fovcld  7537  onminesb  7791  onminsb  7792  tfisg  7849  tfis  7850  limomss  7866  nnlim  7875  ssnlim  7881  resf1ext2b  7931  curry1  8098  curry2  8101  f1o2ndf1  8116  fnwelem  8126  mpoxopn0yelv  8208  tz7.48lem  8427  dif20el  8489  oeordi  8572  oeeulem  8586  oeeui  8587  nnawordex  8622  swoer  8725  eceqoveq  8819  mapsnconst  8889  resixpfo  8933  boxcutc  8938  sdomnen  8977  en0  9014  en0ALT  9015  en0r  9016  en1  9020  dom0  9092  fodomr  9115  dif1enlem  9143  unxpdomlem3  9217  fineqvlem  9225  infn0  9261  fodomfir  9286  f1opwfi  9312  fsuppcolem  9360  fsuppco  9361  mapfienlem1  9364  mapfienlem2  9365  supub  9418  suplub  9419  ordtypelem2  9480  ordtypelem3  9481  ordtypelem6  9484  ordtypelem7  9485  wemapso2lem  9513  wdom2d  9541  brwdom3  9543  ixpiunwdom  9551  inf3lem2  9597  inf3lem6  9601  oancom  9619  infdifsn  9625  cantnfp1lem3  9648  cantnflem3  9659  cantnflem4  9660  oef1o  9666  cnfcom3  9672  tctr  9706  frinsg  9722  tz9.12lem3  9760  scottex  9858  cardid2  9938  infxpenlem  9996  acni3  10030  cardaleph  10072  iscard3  10076  dfac5lem4  10109  dfac5lem5  10110  kmlem1  10133  cofsmo  10252  fin4en1  10292  enfin2i  10304  fin23lem28  10323  fin23lem38  10332  isf32lem6  10341  enfin1ai  10367  hsmexlem2  10410  hsmexlem4  10412  domtriomlem  10425  axdc2lem  10431  axdc3lem2  10434  ac6num  10462  zorn2lem2  10480  brdom3  10511  alephval2  10556  alephreg  10566  pwcfsdom  10567  smobeth  10570  fpwwe2lem5  10619  fpwwe2lem12  10626  canthp1lem2  10637  pwfseqlem3  10644  hargch  10657  winalim2  10680  gchina  10683  inar1  10759  0npi  10866  mulclpi  10877  mulcanpi  10884  nlt1pi  10890  nqereu  10913  prcdnq  10977  prnmax  10979  ltresr2  11125  axrnegex  11146  axpre-sup  11153  eluz2gt1  12943  1nuz2  12947  zsupss  12960  rpgt0  13028  ixxss1  13389  ixxss2  13390  ixxss12  13391  lbioo  13402  ubioo  13403  iccss2  13443  iccssico2  13446  elfzuz3  13548  serge0  14092  expge0  14134  expge1  14135  expaddzlem  14141  hashrabsn1  14410  hashfun  14474  cshinj  14848  relexpuzrel  15089  shftfn  15110  01sqrexlem6  15298  rlimss  15553  lo1dm  15570  o1dm  15581  rlimrege0  15630  fsumf1o  15774  fsumge0  15847  incexc2  15892  supcvg  15910  fprodf1o  16000  divalglem9  16458  bitsfzolem  16491  bitsf1  16503  gcdcllem1  16556  bezout  16600  nprm  16745  dvdsprm  16761  coprm  16769  dfphi2  16832  phimullem  16837  phisum  16849  expnprm  16961  prmreclem2  16976  prmreclem5  16979  1arith  16986  4sqlem18  17021  vdwnnlem3  17056  ramtlecl  17059  rami  17074  0ram  17079  ramub1lem1  17085  prmgaplem5  17114  acsfiel  17709  isacs1i  17712  catlid  17738  catrid  17739  fullfo  17970  fthf1  17975  fthoppc  17981  invfuc  18033  prslem  18352  oduprs  18355  posi  18372  tleile  18474  resspos  18484  resstos  18485  dlatmjdi  18578  pslem  18627  tsrlin  18640  cnvtsr  18643  tsrdir  18659  mndid  18801  mhmf  18846  mhmlin  18850  mhm0  18851  mndind  18886  grpinvex  19009  grplinv  19055  mulgz  19167  mulgdirlem  19170  mulgdir  19171  mulgass  19176  nsgbi  19222  nmzbi  19229  ghmf  19289  ghmlin  19290  conjnsg  19323  gimf1o  19332  gagrpid  19363  gaf  19364  gaass  19366  psgnunilem5  19563  odid  19607  odf1o2  19642  gexid  19650  sylow1lem4  19670  pj1id  19768  efgredeu  19821  ablcmn  19856  cmncom  19867  mulgdi  19895  torsubg  19923  cyggenod2  19954  cygctb  19961  ghmcyg  19965  dprdf1o  20103  ablfacrplem  20136  ablfaclem2  20157  ablfac2  20160  simpg2nsg  20167  fincygsubgodexd  20184  ogrpinv0le  20205  ogrpsub  20206  ogrpaddlt  20207  crngmgp  20322  rnghmmgmhm  20524  rhmmhm  20560  rhmghm  20564  rimf1o  20574  nzrnz  20597  0ringbas  20611  subrgss  20656  subrg1cl  20664  rnghmsubcsetclem1  20715  zrinitorngc  20726  zrtermorngc  20727  rhmsubcsetclem1  20744  ringcinv  20755  zrtermoringc  20759  rrgeq0i  20783  domneq0  20792  domnrrg  20796  drngunit  20817  isdrng4  20824  fldcrngd  20827  drngmgp  20830  drngid  20831  drngdomn  20834  issubdrg  20862  fldhmsubc  20867  fldsdrgfld  20880  cntzsdrg  20884  abvge0  20899  srngcnv  20929  orngsqr  20948  ornglmulle  20949  orngrmulle  20950  ofldtos  20955  ofldlt1  20957  suborng  20958  subofld  20959  lmhmlin  21135  lmimf1o  21163  lvecdrng  21205  lspsolvlem  21245  islbs3  21258  lbsextlem3  21263  2idlelbas  21382  2idlcpblrng  21389  prmidl0  21457  qsidomlem1  21459  zringunit  21595  prmirredlem  21601  irinitoringc  21608  znidomb  21690  cygzn  21699  ofldchr  21705  psgndiflemB  21729  pjf  21842  frlmsslsp  21925  frlmlbs  21926  f1lindf  21951  assalem  21986  psrbaglefi  22055  psrbagleadd1  22057  mplelsfi  22123  mplsubrglem  22132  mplcoe1  22167  mplbas2  22172  opsrtoslem2  22186  mhpmulcl  22291  psdmul  22308  coe1mul2  22409  pmatcoe1fsupp  22837  toponuni  23050  tpsuni  23072  mretopd  23228  neips  23249  neiptoptop  23267  neiptopnei  23268  perflp  23290  perfi  23291  cnf  23382  cnpf  23383  cnpimaex  23392  cnima  23401  t0sep  23460  t1ficld  23463  hausnei  23464  pnrmcld  23478  cnrmi  23496  cmpcov  23525  tgcmp  23537  hauscmplem  23542  connclo  23551  1stcclb  23580  2ndcdisj  23592  llyi  23610  nllyi  23611  ptpjpre1  23707  ptpjcn  23747  ptpjopn  23748  ptclsg  23751  dfac14  23754  txdis1cn  23771  pthaus  23774  hauseqlcld  23782  txkgen  23788  xkococn  23796  txconn  23825  hmeocnvcn  23897  fbssfi  23973  filss  23989  uffixfr  24059  flimneiss  24102  flimelbas  24104  flimfnfcls  24164  alexsubb  24182  alexsubALT  24187  ptcmplem2  24189  ptcmplem3  24190  ptcmplem4  24191  tmdgsum2  24232  ghmcnp  24251  tgpt0  24255  qustgplem  24257  istdrg2  24314  vscacn  24322  tvctdrg  24329  uspreg  24409  ucncn  24420  neipcfilu  24431  cuspcvg  24436  psmetxrge0  24449  isxmet2d  24463  prdsxmetlem  24504  imasdsf1olem  24509  xmstopn  24587  mstopn  24588  stdbdxmet  24651  prdsxmslem2  24665  nrgabv  24797  nmvs  24812  nvclvec  24833  nmoge0  24857  nghmcl  24863  nmoi  24864  nghmghm  24870  nmhmlmhm  24885  nmhmnghm  24886  icccmp  24962  xrge0gsumle  24970  metds0  24987  metdstri  24988  metdsre  24990  metdseq0  24991  metdscnlem  24992  metnrmlem1a  24995  icopnfcnv  25080  xrhmeo  25084  pcoval1  25151  cvslvec  25263  cvsunit  25269  recvs  25284  cphreccllem  25316  cphsscph  25389  cmetcvg  25423  lmle  25439  cmscmet  25484  cmetcusp1  25491  hlcph  25502  minveclem4  25570  ivthlem3  25591  ovolmge0  25615  ovolicc1  25654  ovolicc2lem3  25657  ovolicc2lem5  25659  dyadmbl  25738  i1ff  25814  i1frn  25815  i1fima2  25817  itg2monolem1  25888  dvnres  26069  c1liplem1  26134  c1lip2  26136  dvge0  26144  lhop1lem  26151  itgsubstlem  26186  fta1glem2  26305  fta1b  26308  idomrootle  26309  plyf  26334  plypf1  26348  plyadd  26353  plymul  26354  coeeu  26361  dgrlem  26365  coeid  26374  elqaalem3  26461  aareccl  26466  eff1olem  26689  relogf1o  26707  logdmn0  26781  logcnlem2  26784  logcnlem3  26785  efopnlem1  26797  efopnlem2  26798  logtayl2  26803  cxpcn3lem  26888  cxpcn3  26889  logbgcd1irr  26935  atandmneg  27047  atandmcj  27050  efiatan2  27058  cosatan  27062  cosatanne0  27063  dvatan  27076  areage0  27104  cxp2lim  27117  jensenlem2  27128  jensen  27129  eldmgm  27162  dmgmaddn0  27163  dmlogdmgm  27164  lgamgulmlem2  27170  lgamgulmlem3  27171  lgamgulmlem5  27173  lgambdd  27177  lgamucov  27178  ftalem3  27215  efnnfsumcl  27243  efchtdvds  27299  sqff1o  27322  fsumdvdsdiaglem  27323  dvdsppwf1o  27326  dvdsflf1o  27327  musum  27331  muinv  27333  mpodvdsmulf1o  27334  dvdsmulf1o  27336  lgsfle1  27446  lgsle1  27452  lgsdirprm  27471  lgsne0  27475  lgseisenlem3  27517  lgseisenlem4  27518  lgsquadlem1  27520  lgsquadlem2  27521  chebbnd1  27612  chtppilim  27615  chpchtlim  27619  chpo1ub  27620  dchrmusumlema  27633  dchrvmasumlem1  27635  dchrisum0lema  27654  dchrisum0lem2a  27657  logsqvma  27682  selberg3lem2  27698  pntrsumo1  27705  pnt2  27753  ostthlem1  27767  ostth3  27778  ltsval2  27796  leftlt  28022  rightgt  28023  precsexlem8  28383  precsexlem9  28384  precsexlem11  28386  elons2  28427  onleft  28429  ltonold  28430  oncutleft  28432  oncutlt  28433  zcuts0  28577  axtgcgrrflx  28707  axtgcgrid  28708  axtgsegcon  28709  axtg5seg  28710  axtgbtwnid  28711  axtgpasch  28712  axtgcont1  28713  tglng  28791  axcontlem7  29286  axcontlem10  29289  upgrle  29406  umgredg2  29416  lfgredgge2  29440  usgredg2ALT  29509  usgr1vr  29571  usgrexmpledg  29578  upgrres1  29629  fusgrvtxfi  29635  vtxnbuvtx  29707  cusgrcplgr  29736  vdumgr0  29796  vtxdgoddnumeven  29869  trlres  30014  usgr2pth  30079  cyclispthon  30119  clwwlknlen  30349  clwwnonrepclwwnon  30662  2clwwlk2  30665  ablocom  30866  phpar2  31141  cbncms  31183  hlph  31207  hcaucvg  31504  hlimconvi  31509  shaddcl  31535  shmulcl  31536  chlimi  31552  chcompl  31560  choc1  31645  nmopre  32188  cnopc  32231  lnopl  32232  unop  32233  hmop  32240  cnfnc  32248  lnfnl  32249  nlelshi  32378  cnlnadjlem5  32389  elpjidm  32502  mdslle1i  32635  mdslle2i  32636  atcv0  32660  aciunf1lem  32973  padct  33029  ssnnssfz  33098  ccatf1  33235  swrdrndisj  33243  ressprs  33252  pwrssmgc  33286  wrdpmtrlast  33379  cyc3evpm  33436  cycpmgcl  33439  cycpmconjslem2  33441  cyc3conja  33443  isarchi3  33473  archirng  33474  archirngz  33475  archiabllem1a  33477  archiabllem1b  33478  archiabllem2a  33480  archiabllem2c  33481  archiabllem2b  33482  archiabl  33484  isarchiofld  33485  elrgspnlem1  33528  elrgspnlem2  33529  elrgspnlem4  33531  elrgspnsubrun  33535  ricnzr1  33574  ricdomn1  33575  nn0omnd  33630  quslsm  33680  nsgmgclem  33686  nsgmgc  33687  mxidlirred  33721  krull  33727  ufdprmidl  33797  1arithufdlem4  33803  extvfvcl  33892  mplvrpmlem  33899  mplvrpmga  33901  sradrng  33938  extdg1id  34022  ply1annnr  34059  madjusmdetlem4  34186  qtophaus  34192  crefi  34203  cmpcref  34206  cmppcmp  34214  pcmplfin  34216  zart0  34235  tpr2rico  34268  rge0scvg  34305  zrhunitpreima  34332  qqhrhm  34345  esummono  34410  gsumesum  34415  esumrnmpt2  34424  esumpinfval  34429  esumpcvgval  34434  esumpmono  34435  0elsiga  34470  sigaclcu  34473  issgon  34479  inelpisys  34510  ldsysgenld  34516  ldgenpisyslem1  34519  sxuni  34549  isrnmeas  34556  measvuni  34570  measssd  34571  ddemeas  34592  imambfm  34618  elmbfmvol2  34623  dya2icoseg2  34634  omssubaddlem  34655  omssubadd  34656  carsgsigalem  34671  pmeasmono  34680  sibfinima  34695  oddpwdc  34710  oddpwdcv  34711  eulerpartlemf  34726  eulerpartlemt  34727  eulerpartlemr  34730  eulerpartlemgvv  34732  eulerpartlemgs2  34736  fiblem  34754  probtot  34768  ballotlem4  34855  ballotlem5  34856  ballotlemfrc  34883  ballotlemirc  34888  ballotth  34894  hgt750lemb  35009  bnj642  35103  bnj643  35104  bnj645  35105  bnj707  35110  bnj1379  35184  bnj1538  35209  bnj110  35212  bnj93  35217  bnj906  35284  bnj1006  35314  bnj1110  35336  bnj1121  35339  bnj1204  35366  bnj1321  35381  bnj1364  35382  bnj1398  35388  bnj1450  35404  bnj1312  35412  bnj1501  35421  bnj1523  35425  elscottrank  35480  elscottrankss  35482  tz9.1regs  35513  onvfowev  35566  0nn0m1nnn0  35570  subfacp1lem3  35640  subfacp1lem5  35642  pconncn  35682  connpconn  35693  cvmcov  35721  cvmliftlem1  35743  cvmliftlem10  35752  cvmlift2lem11  35771  cvmlift2lem12  35772  msubff1  36014  mvhf1  36017  mthmpps  36040  mclspps  36042  fundmpss  36225  funpartfun  36401  fnetg  36822  neibastop1  36836  filnetlem3  36857  onint1  36926  weiunlem  36940  weiunpo  36942  weiunse  36945  bj-nnfa  37319  bj-idres  37770  bj-rvecrr  37907  icorempo  37963  pibt2  38029  wl-nfeqfb  38157  phpreu  38221  fin2solem  38223  fin2so  38224  lindsenlbs  38232  matunitlindflem1  38233  matunitlindflem2  38234  matunitlindf  38235  ptrest  38236  poimirlem1  38238  poimirlem2  38239  poimirlem3  38240  poimirlem4  38241  poimirlem5  38242  poimirlem6  38243  poimirlem7  38244  poimirlem8  38245  poimirlem9  38246  poimirlem10  38247  poimirlem11  38248  poimirlem12  38249  poimirlem13  38250  poimirlem14  38251  poimirlem15  38252  poimirlem16  38253  poimirlem17  38254  poimirlem18  38255  poimirlem19  38256  poimirlem20  38257  poimirlem21  38258  poimirlem22  38259  poimirlem23  38260  poimirlem24  38261  poimirlem26  38263  poimirlem27  38264  poimirlem29  38266  poimirlem31  38268  mblfinlem2  38275  dvtan  38287  itg2gt0cn  38292  ftc1anclem7  38316  ftc1anclem8  38317  ftc1anc  38318  cover2  38332  indexa  38350  istotbnd3  38388  sstotbnd2  38391  sstotbnd  38392  totbndss  38394  equivtotbnd  38395  isbnd3  38401  totbndbnd  38406  equivbnd  38407  prdsbnd  38410  prdstotbnd  38411  heibor  38438  zrdivrng  38570  crngocom  38618  isfld2  38622  dmncrng  38673  eqvrelrel  39298  disjrel  39447  disjdmqscossss  39523  prter2  39623  toycom  39715  lsateln0  39737  lpssat  39755  lssat  39758  oposlem  39924  olop  39956  omllaw  39985  cvlexch1  40070  dihpN  42078  mapdordlem2  42379  linvh  42831  idomnnzpownz  42867  idomnnzgmulnz  42868  aks6d1c5lem2  42873  deg1pow  42876  redvmptabs  43089  readvrec2  43090  readvrec  43091  mhphflem  43298  prjspertr  43307  nacsfg  43406  nacsfix  43413  mzpindd  43447  diophrw  43460  diophrex  43476  rexzrexnn0  43501  pell1234qrdich  43558  rmspecnonsq  43604  rmspecfund  43606  rmspecpos  43613  monotoddzzfi  43639  ltrmxnn0  43646  rmxnn  43648  jm2.23  43693  jm3.1lem2  43715  dnnumch3  43744  lnmlssfg  43777  lnmlmic  43785  lnrlnm  43810  lnr2i  43813  lpirlnr  43814  hbtlem6  43826  hbt  43827  mnccoe  43835  proot1mul  43891  proot1hash  43892  deg1mhm  43897  ondif1i  43959  limnsuc  43962  cantnfresb  44021  succlg  44025  ntrneifv2  44776  grucollcld  44940  mnurndlem1  44961  ismnushort  44981  radcnvrat  44994  binomcxplemdvbinom  45033  binomcxplemcvg  45034  binomcxplemnotnn0  45036  ordelordALT  45216  2uasbanh  45240  ordelordALTVD  45545  relprel  45630  elixpconstg  45777  rabidim2  45790  disjinfi  45880  supminfxr2  46153  sumnnodd  46316  stoweidlem7  46691  stoweidlem14  46698  stoweidlem16  46700  stoweidlem24  46708  stoweidlem31  46715  stoweidlem54  46738  wallispilem3  46751  fourierdlem42  46833  fourierdlem48  46838  fourierdlem51  46841  fourierdlem64  46854  fourierdlem76  46866  fourierdlem79  46869  fourierdlem81  46871  fourierdlem87  46877  etransclem28  46946  etransclem32  46950  sge0fodjrnlem  47100  hoidmvlelem3  47281  ovolval5lem3  47338  pimrecltpos  47392  pimrecltneg  47408  issmflem  47411  smfaddlem1  47447  smfsuplem1  47495  smfsuplem3  47497  smflimsuplem7  47510  smfliminflem  47514  nfunsnafv  47846  faovcl  47904  tz6.12-2-afv2  47941  tz6.12i-afv2  47947  sprel  48200  evendiv2z  48364  oddp1div2z  48365  2dvdseven  48385  2ndvdsodd  48387  perfectALTVlem1  48453  sbgoldbm  48516  upgrimtrls  48638  upgrimpthslem1  48639  upgrimspths  48642  upgrimcycls  48643  uhgrimisgrgric  48663  gpgprismgr4cycllem2  48828  clintopcllaw  48943  uzlidlring  48967  rngccatidALTV  49004  funcringcsetcALTV2lem7  49028  ringccatidALTV  49038  ringcinvALTV  49042  funcringcsetclem7ALTV  49051  fldhmsubcALTV  49065  ssnn0ssfz  49096  el0ldepsnzr  49214  regt1loggt0  49283  elbigodm  49302  fllogbd  49307  rrx2xpref1o  49465  unilbss  49563  fdomne0  49595  f002  49599  xpco2  49602  imaf1homlem  49852  idemb  49904  uobeq2  50146  thincmo2  50171  thincmoALT  50174  fullthinc  50195  idfudiag1  50270  elsetrecslem  50444