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 ⊢ (𝜑 → 𝜒)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

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

This theorem is used by:  simplbiim  513  xornan  1548  eumo  2605  reurmo  3371  pssne  4052  pssn2lp  4058  ssnpss  4060  eldifn  4085  elinel2  4154  rabsnt  4696  eldifsni  4757  unimax  4909  ssintub  4930  moop2  5484  pwssun  5552  weso  5651  opelxp2  5703  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  7406  fovcld  7539  onminesb  7790  onminsb  7791  tfisg  7848  tfis  7849  limomss  7865  nnlim  7874  ssnlim  7880  resf1ext2b  7930  curry1  8097  curry2  8100  f1o2ndf1  8115  fnwelem  8125  mpoxopn0yelv  8207  tz7.48lem  8426  dif20el  8488  oeordi  8571  oeeulem  8585  oeeui  8586  nnawordex  8621  swoer  8724  eceqoveq  8818  mapsnconst  8888  resixpfo  8932  boxcutc  8937  sdomnen  8976  en0  9013  en0ALT  9014  en0r  9015  en1  9019  dom0  9091  fodomr  9114  dif1enlem  9142  unxpdomlem3  9216  fineqvlem  9224  infn0  9260  fodomfir  9285  f1opwfi  9311  fsuppcolem  9359  fsuppco  9360  mapfienlem1  9363  mapfienlem2  9364  supub  9417  suplub  9418  ordtypelem2  9479  ordtypelem3  9480  ordtypelem6  9483  ordtypelem7  9484  wemapso2lem  9512  wdom2d  9540  brwdom3  9542  ixpiunwdom  9550  inf3lem2  9596  inf3lem6  9600  oancom  9618  infdifsn  9624  cantnfp1lem3  9647  cantnflem3  9658  cantnflem4  9659  oef1o  9665  cnfcom3  9671  tctr  9705  frinsg  9721  tz9.12lem3  9759  scottex  9860  scottexOLD  9861  cardid2  9946  infxpenlem  10004  acni3  10038  cardaleph  10080  iscard3  10084  dfac5lem4  10117  dfac5lem5  10118  kmlem1  10141  cofsmo  10259  fin4en1  10299  enfin2i  10311  fin23lem28  10330  fin23lem38  10339  isf32lem6  10348  enfin1ai  10374  hsmexlem2  10417  hsmexlem4  10419  domtriomlem  10432  axdc2lem  10438  axdc3lem2  10441  ac6num  10469  zorn2lem2  10487  brdom3  10518  alephval2  10563  alephreg  10573  pwcfsdom  10574  smobeth  10577  fpwwe2lem5  10626  fpwwe2lem12  10633  canthp1lem2  10644  pwfseqlem3  10651  hargch  10664  winalim2  10687  gchina  10690  inar1  10766  0npi  10873  mulclpi  10884  mulcanpi  10891  nlt1pi  10897  nqereu  10920  prcdnq  10984  prnmax  10986  ltresr2  11132  axrnegex  11153  axpre-sup  11160  eluz2gt1  12950  1nuz2  12954  zsupss  12967  rpgt0  13035  ixxss1  13396  ixxss2  13397  ixxss12  13398  lbioo  13409  ubioo  13410  iccss2  13450  iccssico2  13453  elfzuz3  13555  serge0  14099  expge0  14141  expge1  14142  expaddzlem  14148  hashrabsn1  14417  hashfun  14481  cshinj  14855  relexpuzrel  15096  shftfn  15117  01sqrexlem6  15305  rlimss  15560  lo1dm  15577  o1dm  15588  rlimrege0  15637  fsumf1o  15781  fsumge0  15854  incexc2  15899  supcvg  15917  fprodf1o  16007  divalglem9  16465  bitsfzolem  16498  bitsf1  16510  gcdcllem1  16563  bezout  16607  nprm  16752  dvdsprm  16768  coprm  16776  dfphi2  16839  phimullem  16844  phisum  16856  expnprm  16968  prmreclem2  16983  prmreclem5  16986  1arith  16993  4sqlem18  17028  vdwnnlem3  17063  ramtlecl  17066  rami  17081  0ram  17086  ramub1lem1  17092  prmgaplem5  17121  acsfiel  17716  isacs1i  17719  catlid  17745  catrid  17746  fullfo  17977  fthf1  17982  fthoppc  17988  invfuc  18040  prslem  18359  oduprs  18362  posi  18379  tleile  18481  resspos  18491  resstos  18492  dlatmjdi  18585  pslem  18634  tsrlin  18647  cnvtsr  18650  tsrdir  18666  mndid  18808  mhmf  18853  mhmlin  18857  mhm0  18858  mndind  18893  grpinvex  19016  grplinv  19062  mulgz  19174  mulgdirlem  19177  mulgdir  19178  mulgass  19183  nsgbi  19229  nmzbi  19236  ghmf  19296  ghmlin  19297  conjnsg  19330  gimf1o  19339  gagrpid  19370  gaf  19371  gaass  19373  psgnunilem5  19570  odid  19614  odf1o2  19649  gexid  19657  sylow1lem4  19677  pj1id  19775  efgredeu  19828  ablcmn  19863  cmncom  19874  mulgdi  19902  torsubg  19930  cyggenod2  19961  cygctb  19968  ghmcyg  19972  dprdf1o  20110  ablfacrplem  20143  ablfaclem2  20164  ablfac2  20167  simpg2nsg  20174  fincygsubgodexd  20191  ogrpinv0le  20212  ogrpsub  20213  ogrpaddlt  20214  crngmgp  20329  rnghmmgmhm  20532  rhmmhm  20569  rhmghm  20573  rimf1o  20588  nzrnz  20623  0ringbas  20637  subrgss  20682  subrg1cl  20690  rnghmsubcsetclem1  20741  zrinitorngc  20752  zrtermorngc  20753  rhmsubcsetclem1  20770  ringcinv  20781  zrtermoringc  20785  rrgeq0i  20809  domneq0  20818  domnrrg  20822  drngunit  20843  isdrng4  20850  fldcrngd  20853  drngmgp  20856  drngid  20857  drngdomn  20860  issubdrg  20894  fldhmsubc  20899  fldsdrgfld  20912  cntzsdrg  20916  abvge0  20931  srngcnv  20961  orngsqr  20980  ornglmulle  20981  orngrmulle  20982  ofldtos  20987  ofldlt1  20989  suborng  20990  subofld  20991  lmhmlin  21167  lmimf1o  21195  lvecdrng  21237  lspsolvlem  21277  islbs3  21290  lbsextlem3  21295  2idlelbas  21414  2idlcpblrng  21421  prmidl0  21489  qsidomlem1  21491  zringunit  21627  prmirredlem  21633  irinitoringc  21640  znidomb  21722  cygzn  21731  ofldchr  21737  psgndiflemB  21761  pjf  21874  frlmsslsp  21957  frlmlbs  21958  f1lindf  21983  assalem  22018  psrbaglefi  22087  psrbagleadd1  22089  mplelsfi  22155  mplsubrglem  22164  mplcoe1  22199  mplbas2  22204  opsrtoslem2  22218  mhpmulcl  22323  psdmul  22340  coe1mul2  22441  pmatcoe1fsupp  22869  toponuni  23082  tpsuni  23104  mretopd  23260  neips  23281  neiptoptop  23299  neiptopnei  23300  perflp  23322  perfi  23323  cnf  23414  cnpf  23415  cnpimaex  23424  cnima  23433  t0sep  23492  t1ficld  23495  hausnei  23496  pnrmcld  23510  cnrmi  23528  cmpcov  23557  tgcmp  23569  hauscmplem  23574  connclo  23583  1stcclb  23612  2ndcdisj  23624  llyi  23642  nllyi  23643  ptpjpre1  23739  ptpjcn  23779  ptpjopn  23780  ptclsg  23783  dfac14  23786  txdis1cn  23803  pthaus  23806  hauseqlcld  23814  txkgen  23820  xkococn  23828  txconn  23857  hmeocnvcn  23929  fbssfi  24005  filss  24021  uffixfr  24091  flimneiss  24134  flimelbas  24136  flimfnfcls  24196  alexsubb  24214  alexsubALT  24219  ptcmplem2  24221  ptcmplem3  24222  ptcmplem4  24223  tmdgsum2  24264  ghmcnp  24283  tgpt0  24287  qustgplem  24289  istdrg2  24346  vscacn  24354  tvctdrg  24361  uspreg  24441  ucncn  24452  neipcfilu  24463  cuspcvg  24468  psmetxrge0  24481  isxmet2d  24495  prdsxmetlem  24536  imasdsf1olem  24541  xmstopn  24619  mstopn  24620  stdbdxmet  24683  prdsxmslem2  24697  nrgabv  24829  nmvs  24844  nvclvec  24865  nmoge0  24889  nghmcl  24895  nmoi  24896  nghmghm  24902  nmhmlmhm  24917  nmhmnghm  24918  icccmp  24994  xrge0gsumle  25002  metds0  25019  metdstri  25020  metdsre  25022  metdseq0  25023  metdscnlem  25024  metnrmlem1a  25027  icopnfcnv  25112  xrhmeo  25116  pcoval1  25183  cvslvec  25295  cvsunit  25301  recvs  25316  cphreccllem  25348  cphsscph  25421  cmetcvg  25455  lmle  25471  cmscmet  25516  cmetcusp1  25523  hlcph  25534  minveclem4  25602  ivthlem3  25623  ovolmge0  25647  ovolicc1  25686  ovolicc2lem3  25689  ovolicc2lem5  25691  dyadmbl  25770  i1ff  25846  i1frn  25847  i1fima2  25849  itg2monolem1  25920  dvnres  26101  c1liplem1  26166  c1lip2  26168  dvge0  26176  lhop1lem  26183  itgsubstlem  26218  fta1glem2  26337  fta1b  26340  idomrootle  26341  plyf  26366  plypf1  26380  plyadd  26385  plymul  26386  coeeu  26393  dgrlem  26397  coeid  26406  elqaalem3  26493  aareccl  26500  eff1olem  26724  relogf1o  26742  logdmn0  26816  logcnlem2  26819  logcnlem3  26820  efopnlem1  26832  efopnlem2  26833  logtayl2  26838  cxpcn3lem  26923  cxpcn3  26924  logbgcd1irr  26970  atandmneg  27082  atandmcj  27085  efiatan2  27093  cosatan  27097  cosatanne0  27098  dvatan  27111  areage0  27139  cxp2lim  27152  jensenlem2  27163  jensen  27164  eldmgm  27197  dmgmaddn0  27198  dmlogdmgm  27199  lgamgulmlem2  27205  lgamgulmlem3  27206  lgamgulmlem5  27208  lgambdd  27212  lgamucov  27213  ftalem3  27250  efnnfsumcl  27278  efchtdvds  27334  sqff1o  27357  fsumdvdsdiaglem  27358  dvdsppwf1o  27361  dvdsflf1o  27362  musum  27366  muinv  27368  mpodvdsmulf1o  27369  dvdsmulf1o  27371  lgsfle1  27481  lgsle1  27487  lgsdirprm  27506  lgsne0  27510  lgseisenlem3  27552  lgseisenlem4  27553  lgsquadlem1  27555  lgsquadlem2  27556  chebbnd1  27647  chtppilim  27650  chpchtlim  27654  chpo1ub  27655  dchrmusumlema  27668  dchrvmasumlem1  27670  dchrisum0lema  27689  dchrisum0lem2a  27692  logsqvma  27717  selberg3lem2  27733  pntrsumo1  27740  pnt2  27788  ostthlem1  27802  ostth3  27813  ltsval2  27831  leftlt  28057  rightgt  28058  precsexlem8  28418  precsexlem9  28419  precsexlem11  28421  elons2  28462  onleft  28464  ltonold  28465  oncutleft  28467  oncutlt  28468  zcuts0  28612  axtgcgrrflx  28742  axtgcgrid  28743  axtgsegcon  28744  axtg5seg  28745  axtgbtwnid  28746  axtgpasch  28747  axtgcont1  28748  tglng  28826  axcontlem7  29331  axcontlem10  29334  upgrle  29451  umgredg2  29461  lfgredgge2  29485  usgredg2ALT  29554  usgr1vr  29616  usgrexmpledg  29623  upgrres1  29674  fusgrvtxfi  29680  vtxnbuvtx  29752  cusgrcplgr  29781  vdumgr0  29841  vtxdgoddnumeven  29914  trlres  30059  usgr2pth  30124  cyclispthon  30164  clwwlknlen  30394  clwwnonrepclwwnon  30707  2clwwlk2  30710  ablocom  30911  phpar2  31186  cbncms  31228  hlph  31252  hcaucvg  31549  hlimconvi  31554  shaddcl  31580  shmulcl  31581  chlimi  31597  chcompl  31605  choc1  31690  nmopre  32233  cnopc  32276  lnopl  32277  unop  32278  hmop  32285  cnfnc  32293  lnfnl  32294  nlelshi  32423  cnlnadjlem5  32434  elpjidm  32547  mdslle1i  32680  mdslle2i  32681  atcv0  32705  aciunf1lem  33018  padct  33074  ssnnssfz  33143  ccatf1  33278  swrdrndisj  33286  ressprs  33295  pwrssmgc  33329  wrdpmtrlast  33422  cyc3evpm  33479  cycpmgcl  33482  cycpmconjslem2  33484  cyc3conja  33486  isarchi3  33516  archirng  33517  archirngz  33518  archiabllem1a  33520  archiabllem1b  33521  archiabllem2a  33523  archiabllem2c  33524  archiabllem2b  33525  archiabl  33527  isarchiofld  33528  elrgspnlem1  33571  elrgspnlem2  33572  elrgspnlem4  33574  elrgspnsubrun  33578  ricnzr1  33617  ricdomn1  33618  nn0omnd  33673  quslsm  33723  nsgmgclem  33729  nsgmgc  33730  mxidlirred  33764  krull  33770  ufdprmidl  33840  1arithufdlem4  33846  extvfvcl  33935  mplvrpmlem  33942  mplvrpmga  33944  sradrng  33981  extdg1id  34065  ply1annnr  34102  madjusmdetlem4  34229  qtophaus  34235  crefi  34246  cmpcref  34249  cmppcmp  34257  pcmplfin  34259  zart0  34278  tpr2rico  34311  rge0scvg  34348  zrhunitpreima  34375  qqhrhm  34388  esummono  34453  gsumesum  34458  esumrnmpt2  34467  esumpinfval  34472  esumpcvgval  34477  esumpmono  34478  0elsiga  34513  sigaclcu  34516  issgon  34522  inelpisys  34553  ldsysgenld  34559  ldgenpisyslem1  34562  sxuni  34592  isrnmeas  34599  measvuni  34613  measssd  34614  ddemeas  34635  imambfm  34661  elmbfmvol2  34666  dya2icoseg2  34677  omssubaddlem  34698  omssubadd  34699  carsgsigalem  34714  pmeasmono  34723  sibfinima  34738  oddpwdc  34753  oddpwdcv  34754  eulerpartlemf  34769  eulerpartlemt  34770  eulerpartlemr  34773  eulerpartlemgvv  34775  eulerpartlemgs2  34779  fiblem  34797  probtot  34811  ballotlem4  34898  ballotlem5  34899  ballotlemfrc  34926  ballotlemirc  34931  ballotth  34937  hgt750lemb  35052  bnj642  35146  bnj643  35147  bnj645  35148  bnj707  35153  bnj1379  35227  bnj1538  35252  bnj110  35255  bnj93  35260  bnj906  35327  bnj1006  35357  bnj1110  35379  bnj1121  35382  bnj1204  35409  bnj1321  35424  bnj1364  35425  bnj1398  35431  bnj1450  35447  bnj1312  35455  bnj1501  35464  bnj1523  35468  elscottrank  35523  elscottrankss  35525  tz9.1regs  35555  onvfowev  35608  0nn0m1nnn0  35612  subfacp1lem3  35682  subfacp1lem5  35684  pconncn  35724  connpconn  35735  cvmcov  35763  cvmliftlem1  35785  cvmliftlem10  35794  cvmlift2lem11  35813  cvmlift2lem12  35814  msubff1  36056  mvhf1  36059  mthmpps  36082  mclspps  36084  fundmpss  36267  funpartfun  36443  fnetg  36884  neibastop1  36898  filnetlem3  36919  onint1  36988  weiunlem  37002  weiunpo  37004  weiunse  37007  bj-nnfa  37381  bj-idres  37832  bj-rvecrr  37969  icorempo  38025  pibt2  38091  wl-nfeqfb  38219  phpreu  38283  fin2solem  38285  fin2so  38286  lindsenlbs  38294  matunitlindflem1  38295  matunitlindflem2  38296  matunitlindf  38297  ptrest  38298  poimirlem1  38300  poimirlem2  38301  poimirlem3  38302  poimirlem4  38303  poimirlem5  38304  poimirlem6  38305  poimirlem7  38306  poimirlem8  38307  poimirlem9  38308  poimirlem10  38309  poimirlem11  38310  poimirlem12  38311  poimirlem13  38312  poimirlem14  38313  poimirlem15  38314  poimirlem16  38315  poimirlem17  38316  poimirlem18  38317  poimirlem19  38318  poimirlem20  38319  poimirlem21  38320  poimirlem22  38321  poimirlem23  38322  poimirlem24  38323  poimirlem26  38325  poimirlem27  38326  poimirlem29  38328  poimirlem31  38330  mblfinlem2  38337  dvtan  38349  itg2gt0cn  38354  ftc1anclem7  38378  ftc1anclem8  38379  ftc1anc  38380  cover2  38394  indexa  38412  istotbnd3  38450  sstotbnd2  38453  sstotbnd  38454  totbndss  38456  equivtotbnd  38457  isbnd3  38463  totbndbnd  38468  equivbnd  38469  prdsbnd  38472  prdstotbnd  38473  heibor  38500  zrdivrng  38632  crngocom  38680  isfld2  38684  dmncrng  38735  eqvrelrel  39358  disjrel  39507  disjdmqscossss  39583  prter2  39683  toycom  39775  lsateln0  39797  lpssat  39815  lssat  39818  oposlem  39984  olop  40016  omllaw  40045  cvlexch1  40130  dihpN  42138  mapdordlem2  42439  linvh  42891  idomnnzpownz  42927  idomnnzgmulnz  42928  aks6d1c5lem2  42933  deg1pow  42936  redvmptabs  43149  readvrec2  43150  readvrec  43151  mhphflem  43356  prjspertr  43365  nacsfg  43464  nacsfix  43471  mzpindd  43505  diophrw  43518  diophrex  43534  rexzrexnn0  43559  pell1234qrdich  43616  rmspecnonsq  43662  rmspecfund  43664  rmspecpos  43671  monotoddzzfi  43697  ltrmxnn0  43704  rmxnn  43706  jm2.23  43751  jm3.1lem2  43773  dnnumch3  43802  lnmlssfg  43835  lnmlmic  43843  lnrlnm  43868  lnr2i  43871  lpirlnr  43872  hbtlem6  43884  hbt  43885  mnccoe  43893  proot1mul  43949  proot1hash  43950  deg1mhm  43955  ondif1i  44017  limnsuc  44020  cantnfresb  44079  succlg  44083  ntrneifv2  44834  grucollcld  44998  mnurndlem1  45019  ismnushort  45039  radcnvrat  45052  binomcxplemdvbinom  45091  binomcxplemcvg  45092  binomcxplemnotnn0  45094  ordelordALT  45274  2uasbanh  45298  ordelordALTVD  45603  relprel  45688  elixpconstg  45835  rabidim2  45848  disjinfi  45938  supminfxr2  46211  sumnnodd  46374  stoweidlem7  46749  stoweidlem14  46756  stoweidlem16  46758  stoweidlem24  46766  stoweidlem31  46773  stoweidlem54  46796  wallispilem3  46809  fourierdlem42  46891  fourierdlem48  46896  fourierdlem51  46899  fourierdlem64  46912  fourierdlem76  46924  fourierdlem79  46927  fourierdlem81  46929  fourierdlem87  46935  etransclem28  47004  etransclem32  47008  sge0fodjrnlem  47158  hoidmvlelem3  47339  ovolval5lem3  47396  pimrecltpos  47450  pimrecltneg  47466  issmflem  47469  smfaddlem1  47505  smfsuplem1  47553  smfsuplem3  47555  smflimsuplem7  47568  smfliminflem  47572  nfunsnafv  47907  faovcl  47965  tz6.12-2-afv2  48002  tz6.12i-afv2  48008  sprel  48261  evendiv2z  48425  oddp1div2z  48426  2dvdseven  48446  2ndvdsodd  48448  perfectALTVlem1  48514  sbgoldbm  48577  upgrimtrls  48699  upgrimpthslem1  48700  upgrimspths  48703  upgrimcycls  48704  uhgrimisgrgric  48724  gpgprismgr4cycllem2  48889  clintopcllaw  49004  uzlidlring  49028  rngccatidALTV  49065  funcringcsetcALTV2lem7  49089  ringccatidALTV  49099  ringcinvALTV  49103  funcringcsetclem7ALTV  49112  fldhmsubcALTV  49126  ssnn0ssfz  49157  el0ldepsnzr  49275  regt1loggt0  49344  elbigodm  49363  fllogbd  49368  rrx2xpref1o  49526  unilbss  49624  fdomne0  49656  f002  49660  xpco2  49663  imaf1homlem  49913  idemb  49965  uobeq2  50207  thincmo2  50232  thincmoALT  50235  fullthinc  50256  idfudiag1  50331  elsetrecslem  50505  alseueu  50643