Theorem simprbi 497

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 216	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simprd 495	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  simplbiim  504  xornan  1521  eumo  2579  reurmo  3346  pssne  4040  pssn2lp  4045  ssnpss  4047  eldifn  4073  elinel2  4143  rabsnt  4676  eldifsni  4734  unimax  4888  ssintub  4909  moop2  5448  pwssun  5514  weso  5613  opelxp2  5665  predpo  6279  frpoinsg  6299  ordwe  6328  funmo  6506  funopg  6524  funun  6536  fununi  6565  funimaexg  6577  fndm  6593  frn  6667  f1ss  6733  f1ssr  6734  forn  6747  f1f1orn  6783  f1orescnv  6787  f1imacnv  6788  funcocnv2  6797  dffv2  6927  exfo  7049  foelrn  7051  foelrnf  7052  isorel  7272  isoini2  7285  f1ofveu  7352  fovcld  7485  onminesb  7738  onminsb  7739  tfisg  7796  tfis  7797  limomss  7813  nnlim  7822  ssnlim  7828  resf1ext2b  7877  curry1  8045  curry2  8048  f1o2ndf1  8063  fnwelem  8072  mpoxopn0yelv  8154  tz7.48lem  8371  dif20el  8431  oeordi  8514  oeeulem  8528  oeeui  8529  nnawordex  8564  swoer  8666  eceqoveq  8760  mapsnconst  8831  resixpfo  8875  boxcutc  8880  sdomnen  8919  en0  8956  en0ALT  8957  en0r  8958  en1  8962  dom0  9034  fodomr  9057  dif1enlem  9085  unxpdomlem3  9159  fineqvlem  9167  infn0  9203  fodomfir  9229  f1opwfi  9257  fsuppcolem  9305  fsuppco  9306  mapfienlem1  9309  mapfienlem2  9310  supub  9363  suplub  9364  ordtypelem2  9425  ordtypelem3  9426  ordtypelem6  9429  ordtypelem7  9430  wemapso2lem  9458  wdom2d  9486  brwdom3  9488  ixpiunwdom  9496  inf3lem2  9539  inf3lem6  9543  oancom  9561  infdifsn  9567  cantnfp1lem3  9590  cantnflem3  9601  cantnflem4  9602  oef1o  9608  cnfcom3  9614  tctr  9648  frinsg  9664  tz9.12lem3  9702  scottex  9798  cardid2  9866  infxpenlem  9924  acni3  9958  cardaleph  10000  iscard3  10004  dfac5lem4  10037  dfac5lem5  10038  dfac5lem4OLD  10039  kmlem1  10062  cofsmo  10180  fin4en1  10220  enfin2i  10232  fin23lem28  10251  fin23lem38  10260  isf32lem6  10269  enfin1ai  10295  hsmexlem2  10338  hsmexlem4  10340  domtriomlem  10353  axdc2lem  10359  axdc3lem2  10362  ac6num  10390  zorn2lem2  10408  brdom3  10439  alephval2  10484  alephreg  10494  pwcfsdom  10495  smobeth  10498  fpwwe2lem5  10547  fpwwe2lem12  10554  canthp1lem2  10565  pwfseqlem3  10572  hargch  10585  winalim2  10608  gchina  10611  inar1  10687  0npi  10794  mulclpi  10805  mulcanpi  10812  nlt1pi  10818  nqereu  10841  prcdnq  10905  prnmax  10907  ltresr2  11053  axrnegex  11074  axpre-sup  11081  eluz2gt1  12859  1nuz2  12863  zsupss  12876  rpgt0  12944  ixxss1  13305  ixxss2  13306  ixxss12  13307  lbioo  13318  ubioo  13319  iccss2  13359  iccssico2  13362  elfzuz3  13464  serge0  14007  expge0  14049  expge1  14050  expaddzlem  14056  hashrabsn1  14325  hashfun  14388  cshinj  14762  relexpuzrel  15003  shftfn  15024  01sqrexlem6  15198  rlimss  15453  lo1dm  15470  o1dm  15481  rlimrege0  15530  fsumf1o  15674  fsumge0  15747  incexc2  15792  supcvg  15810  fprodf1o  15900  divalglem9  16359  bitsfzolem  16392  bitsf1  16404  gcdcllem1  16457  bezout  16501  nprm  16646  dvdsprm  16662  coprm  16670  dfphi2  16733  phimullem  16738  phisum  16750  expnprm  16862  prmreclem2  16877  prmreclem5  16880  1arith  16887  4sqlem18  16922  vdwnnlem3  16957  ramtlecl  16960  rami  16975  0ram  16980  ramub1lem1  16986  prmgaplem5  17015  acsfiel  17609  isacs1i  17612  catlid  17638  catrid  17639  fullfo  17870  fthf1  17875  fthoppc  17881  invfuc  17933  prslem  18252  oduprs  18255  posi  18272  tleile  18374  resspos  18384  resstos  18385  dlatmjdi  18478  pslem  18527  tsrlin  18540  cnvtsr  18543  tsrdir  18559  mndid  18701  mhmf  18746  mhmlin  18750  mhm0  18751  mndind  18785  grpinvex  18908  grplinv  18954  mulgz  19067  mulgdirlem  19070  mulgdir  19071  mulgass  19076  nsgbi  19121  nmzbi  19128  ghmf  19184  ghmlin  19185  conjnsg  19218  gimf1o  19227  gagrpid  19258  gaf  19259  gaass  19261  psgnunilem5  19458  odid  19502  odf1o2  19537  gexid  19545  sylow1lem4  19565  pj1id  19663  efgredeu  19716  ablcmn  19751  cmncom  19762  mulgdi  19790  torsubg  19818  cyggenod2  19849  cygctb  19856  ghmcyg  19860  dprdf1o  19998  ablfacrplem  20031  ablfaclem2  20052  ablfac2  20055  simpg2nsg  20062  fincygsubgodexd  20079  ogrpinv0le  20100  ogrpsub  20101  ogrpaddlt  20102  crngmgp  20211  rnghmmgmhm  20412  rhmmhm  20448  rhmghm  20452  rimf1o  20461  nzrnz  20481  0ringbas  20494  subrgss  20538  subrg1cl  20546  rnghmsubcsetclem1  20597  zrinitorngc  20608  zrtermorngc  20609  rhmsubcsetclem1  20626  ringcinv  20637  zrtermoringc  20641  rrgeq0i  20665  domneq0  20674  domnrrg  20679  drngunit  20700  fldcrngd  20708  drngmgp  20711  drngid  20712  drngdomn  20715  issubdrg  20746  fldhmsubc  20751  fldsdrgfld  20764  cntzsdrg  20768  abvge0  20783  srngcnv  20813  orngsqr  20832  ornglmulle  20833  orngrmulle  20834  ofldtos  20839  ofldlt1  20841  suborng  20842  subofld  20843  lmhmlin  21020  lmimf1o  21048  lvecdrng  21090  lspsolvlem  21130  islbs3  21143  lbsextlem3  21148  2idlelbas  21252  2idlcpblrng  21259  zringunit  21454  prmirredlem  21460  irinitoringc  21467  znidomb  21549  cygzn  21558  ofldchr  21564  psgndiflemB  21588  pjf  21701  frlmsslsp  21784  frlmlbs  21785  f1lindf  21810  assalem  21845  psrbaglefi  21914  psrbagleadd1  21916  mplelsfi  21982  mplsubrglem  21991  mplcoe1  22024  mplbas2  22029  opsrtoslem2  22043  mhpmulcl  22124  psdmul  22141  coe1mul2  22243  pmatcoe1fsupp  22675  toponuni  22888  tpsuni  22910  mretopd  23066  neips  23087  neiptoptop  23105  neiptopnei  23106  perflp  23128  perfi  23129  cnf  23220  cnpf  23221  cnpimaex  23230  cnima  23239  t0sep  23298  t1ficld  23301  hausnei  23302  pnrmcld  23316  cnrmi  23334  cmpcov  23363  tgcmp  23375  hauscmplem  23380  connclo  23389  1stcclb  23418  2ndcdisj  23430  llyi  23448  nllyi  23449  ptpjpre1  23545  ptpjcn  23585  ptpjopn  23586  ptclsg  23589  dfac14  23592  txdis1cn  23609  pthaus  23612  hauseqlcld  23620  txkgen  23626  xkococn  23634  txconn  23663  hmeocnvcn  23735  fbssfi  23811  filss  23827  uffixfr  23897  flimneiss  23940  flimelbas  23942  flimfnfcls  24002  alexsubb  24020  alexsubALT  24025  ptcmplem2  24027  ptcmplem3  24028  ptcmplem4  24029  tmdgsum2  24070  ghmcnp  24089  tgpt0  24093  qustgplem  24095  istdrg2  24152  vscacn  24160  tvctdrg  24167  uspreg  24247  ucncn  24258  neipcfilu  24269  cuspcvg  24274  psmetxrge0  24287  isxmet2d  24301  prdsxmetlem  24342  imasdsf1olem  24347  xmstopn  24425  mstopn  24426  stdbdxmet  24489  prdsxmslem2  24503  nrgabv  24635  nmvs  24650  nvclvec  24671  nmoge0  24695  nghmcl  24701  nmoi  24702  nghmghm  24708  nmhmlmhm  24723  nmhmnghm  24724  icccmp  24800  xrge0gsumle  24808  metds0  24825  metdstri  24826  metdsre  24828  metdseq0  24829  metdscnlem  24830  metnrmlem1a  24833  icopnfcnv  24918  xrhmeo  24922  pcoval1  24989  cvslvec  25101  cvsunit  25107  recvs  25122  cphreccllem  25154  cphsscph  25227  cmetcvg  25261  lmle  25277  cmscmet  25322  cmetcusp1  25329  hlcph  25340  minveclem4  25408  ivthlem3  25429  ovolmge0  25453  ovolicc1  25492  ovolicc2lem3  25495  ovolicc2lem5  25497  dyadmbl  25576  i1ff  25652  i1frn  25653  i1fima2  25655  itg2monolem1  25726  dvnres  25907  c1liplem1  25973  c1lip2  25975  dvge0  25983  lhop1lem  25990  itgsubstlem  26027  fta1glem2  26146  fta1b  26149  idomrootle  26150  plyf  26175  plypf1  26189  plyadd  26194  plymul  26195  coeeu  26202  dgrlem  26206  coeid  26215  elqaalem3  26300  aareccl  26305  eff1olem  26528  relogf1o  26546  logdmn0  26620  logcnlem2  26623  logcnlem3  26624  efopnlem1  26636  efopnlem2  26637  logtayl2  26642  cxpcn3lem  26728  cxpcn3  26729  logbgcd1irr  26775  atandmneg  26887  atandmcj  26890  efiatan2  26898  cosatan  26902  cosatanne0  26903  dvatan  26916  areage0  26944  cxp2lim  26958  jensenlem2  26969  jensen  26970  eldmgm  27003  dmgmaddn0  27004  dmlogdmgm  27005  lgamgulmlem2  27011  lgamgulmlem3  27012  lgamgulmlem5  27014  lgambdd  27018  lgamucov  27019  ftalem3  27056  efnnfsumcl  27084  efchtdvds  27140  sqff1o  27163  fsumdvdsdiaglem  27164  dvdsppwf1o  27167  dvdsflf1o  27168  musum  27172  muinv  27174  mpodvdsmulf1o  27175  dvdsmulf1o  27177  lgsfle1  27288  lgsle1  27294  lgsdirprm  27313  lgsne0  27317  lgseisenlem3  27359  lgseisenlem4  27360  lgsquadlem1  27362  lgsquadlem2  27363  chebbnd1  27454  chtppilim  27457  chpchtlim  27461  chpo1ub  27462  dchrmusumlema  27475  dchrvmasumlem1  27477  dchrisum0lema  27496  dchrisum0lem2a  27499  logsqvma  27524  selberg3lem2  27540  pntrsumo1  27547  pnt2  27595  ostthlem1  27609  ostth3  27620  ltsval2  27639  leftlt  27864  rightgt  27865  precsexlem8  28225  precsexlem9  28226  precsexlem11  28228  elons2  28269  onleft  28271  ltonold  28272  oncutleft  28274  oncutlt  28275  zcuts0  28419  axtgcgrrflx  28549  axtgcgrid  28550  axtgsegcon  28551  axtg5seg  28552  axtgbtwnid  28553  axtgpasch  28554  axtgcont1  28555  tglng  28633  axcontlem7  29058  axcontlem10  29061  upgrle  29178  umgredg2  29188  lfgredgge2  29212  usgredg2ALT  29281  usgr1vr  29343  usgrexmpledg  29350  upgrres1  29401  fusgrvtxfi  29407  vtxnbuvtx  29479  cusgrcplgr  29508  vdumgr0  29569  vtxdgoddnumeven  29642  trlres  29787  usgr2pth  29852  cyclispthon  29892  clwwlknlen  30122  clwwnonrepclwwnon  30435  2clwwlk2  30438  ablocom  30639  phpar2  30914  cbncms  30956  hlph  30980  hcaucvg  31277  hlimconvi  31282  shaddcl  31308  shmulcl  31309  chlimi  31325  chcompl  31333  choc1  31418  nmopre  31961  cnopc  32004  lnopl  32005  unop  32006  hmop  32013  cnfnc  32021  lnfnl  32022  nlelshi  32151  cnlnadjlem5  32162  elpjidm  32275  mdslle1i  32408  mdslle2i  32409  atcv0  32433  aciunf1lem  32755  padct  32811  ssnnssfz  32880  ccatf1  33029  swrdrndisj  33037  ressprs  33046  pwrssmgc  33080  wrdpmtrlast  33174  cyc3evpm  33231  cycpmgcl  33234  cycpmconjslem2  33236  cyc3conja  33238  isarchi3  33268  archirng  33269  archirngz  33270  archiabllem1a  33272  archiabllem1b  33273  archiabllem2a  33275  archiabllem2c  33276  archiabllem2b  33277  archiabl  33279  isarchiofld  33280  elrgspnlem1  33323  elrgspnlem2  33324  elrgspnlem4  33326  elrgspnsubrun  33330  isdrng4  33376  nn0omnd  33424  quslsm  33485  nsgmgclem  33491  nsgmgc  33492  prmidl0  33530  qsidomlem1  33532  mxidlirred  33552  krull  33559  ufdprmidl  33621  1arithufdlem4  33627  extvfvcl  33700  mplvrpmlem  33707  mplvrpmga  33709  sradrng  33746  extdg1id  33831  ply1annnr  33868  madjusmdetlem4  33995  qtophaus  34001  crefi  34012  cmpcref  34015  cmppcmp  34023  pcmplfin  34025  zart0  34044  tpr2rico  34077  rge0scvg  34114  zrhunitpreima  34141  qqhrhm  34154  esummono  34219  gsumesum  34224  esumrnmpt2  34233  esumpinfval  34238  esumpcvgval  34243  esumpmono  34244  0elsiga  34279  sigaclcu  34282  issgon  34288  inelpisys  34319  ldsysgenld  34325  ldgenpisyslem1  34328  sxuni  34358  isrnmeas  34365  measvuni  34379  measssd  34380  ddemeas  34401  imambfm  34427  elmbfmvol2  34432  dya2icoseg2  34443  omssubaddlem  34464  omssubadd  34465  carsgsigalem  34480  pmeasmono  34489  sibfinima  34504  oddpwdc  34519  oddpwdcv  34520  eulerpartlemf  34535  eulerpartlemt  34536  eulerpartlemr  34539  eulerpartlemgvv  34541  eulerpartlemgs2  34545  fiblem  34563  probtot  34577  ballotlem4  34664  ballotlem5  34665  ballotlemfrc  34692  ballotlemirc  34697  ballotth  34703  hgt750lemb  34821  bnj642  34912  bnj643  34913  bnj645  34914  bnj707  34919  bnj1379  34993  bnj1538  35018  bnj110  35021  bnj93  35026  bnj906  35093  bnj1006  35123  bnj1110  35145  bnj1121  35148  bnj1204  35175  bnj1321  35190  bnj1364  35191  bnj1398  35197  bnj1450  35213  bnj1312  35221  bnj1501  35230  bnj1523  35234  tz9.1regs  35299  0nn0m1nnn0  35316  subfacp1lem3  35385  subfacp1lem5  35387  pconncn  35427  connpconn  35438  cvmcov  35466  cvmliftlem1  35488  cvmliftlem10  35497  cvmlift2lem11  35516  cvmlift2lem12  35517  msubff1  35759  mvhf1  35762  mthmpps  35785  mclspps  35787  fundmpss  35970  funpartfun  36146  fnetg  36548  neibastop1  36562  filnetlem3  36583  onint1  36652  weiunlem  36666  weiunpo  36668  weiunse  36671  bj-nnfa  37038  bj-idres  37487  bj-rvecrr  37624  icorempo  37678  pibt2  37744  wl-nfeqfb  37872  phpreu  37936  fin2solem  37938  fin2so  37939  lindsenlbs  37947  matunitlindflem1  37948  matunitlindflem2  37949  matunitlindf  37950  ptrest  37951  poimirlem1  37953  poimirlem2  37954  poimirlem3  37955  poimirlem4  37956  poimirlem5  37957  poimirlem6  37958  poimirlem7  37959  poimirlem8  37960  poimirlem9  37961  poimirlem10  37962  poimirlem11  37963  poimirlem12  37964  poimirlem13  37965  poimirlem14  37966  poimirlem15  37967  poimirlem16  37968  poimirlem17  37969  poimirlem18  37970  poimirlem19  37971  poimirlem20  37972  poimirlem21  37973  poimirlem22  37974  poimirlem23  37975  poimirlem24  37976  poimirlem26  37978  poimirlem27  37979  poimirlem29  37981  poimirlem31  37983  mblfinlem2  37990  dvtan  38002  itg2gt0cn  38007  ftc1anclem7  38031  ftc1anclem8  38032  ftc1anc  38033  cover2  38047  indexa  38065  istotbnd3  38103  sstotbnd2  38106  sstotbnd  38107  totbndss  38109  equivtotbnd  38110  isbnd3  38116  totbndbnd  38121  equivbnd  38122  prdsbnd  38125  prdstotbnd  38126  heibor  38153  zrdivrng  38285  crngocom  38333  isfld2  38337  dmncrng  38388  eqvrelrel  39013  disjrel  39162  disjdmqscossss  39238  prter2  39338  toycom  39430  lsateln0  39452  lpssat  39470  lssat  39473  oposlem  39639  olop  39671  omllaw  39700  cvlexch1  39785  dihpN  41793  mapdordlem2  42094  linvh  42546  idomnnzpownz  42582  idomnnzgmulnz  42583  aks6d1c5lem2  42588  deg1pow  42591  redvmptabs  42803  readvrec2  42804  readvrec  42805  mhphflem  43040  prjspertr  43049  nacsfg  43148  nacsfix  43155  mzpindd  43189  diophrw  43202  diophrex  43218  rexzrexnn0  43247  pell1234qrdich  43304  rmspecnonsq  43350  rmspecfund  43352  rmspecpos  43359  monotoddzzfi  43385  ltrmxnn0  43392  rmxnn  43394  jm2.23  43439  jm3.1lem2  43461  dnnumch3  43490  lnmlssfg  43523  lnmlmic  43531  lnrlnm  43556  lnr2i  43559  lpirlnr  43560  hbtlem6  43572  hbt  43573  mnccoe  43581  proot1mul  43637  proot1hash  43638  deg1mhm  43643  ondif1i  43705  limnsuc  43708  cantnfresb  43767  succlg  43771  ntrneifv2  44522  grucollcld  44702  mnurndlem1  44723  ismnushort  44743  radcnvrat  44756  binomcxplemdvbinom  44795  binomcxplemcvg  44796  binomcxplemnotnn0  44798  ordelordALT  44979  2uasbanh  45003  ordelordALTVD  45308  relprel  45393  elixpconstg  45534  rabidim2  45547  disjinfi  45637  supminfxr2  45912  sumnnodd  46075  stoweidlem7  46450  stoweidlem14  46457  stoweidlem16  46459  stoweidlem24  46467  stoweidlem31  46474  stoweidlem54  46497  wallispilem3  46510  fourierdlem42  46592  fourierdlem48  46597  fourierdlem51  46600  fourierdlem64  46613  fourierdlem76  46625  fourierdlem79  46628  fourierdlem81  46630  fourierdlem87  46636  etransclem28  46705  etransclem32  46709  sge0fodjrnlem  46859  hoidmvlelem3  47040  ovolval5lem3  47097  pimrecltpos  47151  pimrecltneg  47167  issmflem  47170  smfaddlem1  47206  smfsuplem1  47254  smfsuplem3  47256  smflimsuplem7  47269  smfliminflem  47273  nfunsnafv  47587  faovcl  47645  tz6.12-2-afv2  47682  tz6.12i-afv2  47688  sprel  47941  evendiv2z  48105  oddp1div2z  48106  2dvdseven  48126  2ndvdsodd  48128  perfectALTVlem1  48194  sbgoldbm  48257  upgrimtrls  48379  upgrimpthslem1  48380  upgrimspths  48383  upgrimcycls  48384  uhgrimisgrgric  48404  gpgprismgr4cycllem2  48569  clintopcllaw  48684  uzlidlring  48708  rngccatidALTV  48745  funcringcsetcALTV2lem7  48769  ringccatidALTV  48779  ringcinvALTV  48783  funcringcsetclem7ALTV  48792  fldhmsubcALTV  48806  ssnn0ssfz  48822  el0ldepsnzr  48940  regt1loggt0  49009  elbigodm  49028  fllogbd  49033  rrx2xpref1o  49191  unilbss  49290  fdomne0  49322  f002  49326  xpco2  49329  imaf1homlem  49579  idemb  49631  uobeq2  49873  thincmo2  49898  thincmoALT  49901  fullthinc  49922  idfudiag1  49997  elsetrecslem  50171