Theorem simprbi 503

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

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

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 402

This theorem is used by:  simplbiim  514  xornan  1549  eumo  2605  reurmo  3370  pssne  4050  pssn2lp  4056  ssnpss  4058  eldifn  4082  elinel2  4151  rabsnt  4695  eldifsni  4756  unimax  4908  ssintub  4929  moop2  5483  pwssun  5551  weso  5650  opelxp2  5702  predpo  6325  frpoinsg  6345  ordwe  6374  funmo  6553  funopg  6571  funun  6583  fununi  6612  funimaexg  6623  fndm  6639  frn  6714  f1ss  6782  f1ssr  6783  forn  6796  f1f1orn  6833  f1orescnv  6837  f1imacnv  6838  funcocnv2  6847  dffv2  6977  exfo  7101  foelrn  7103  foelrnf  7104  isorel  7330  isoini2  7343  f1ofveu  7410  fovcld  7543  onminesb  7795  onminsb  7796  tfisg  7853  tfis  7854  limomss  7870  nnlim  7879  ssnlim  7885  resf1ext2b  7935  curry1  8104  curry2  8107  f1o2ndf1  8122  fnwelem  8132  mpoxopn0yelv  8214  tz7.48lem  8433  dif20el  8495  oeordi  8578  oeeulem  8592  oeeui  8593  nnawordex  8628  swoer  8731  eceqoveq  8825  mapsnconst  8902  resixpfo  8946  boxcutc  8951  sdomnen  8990  en0  9027  en0ALT  9028  en0r  9029  en1  9033  dom0  9106  fodomr  9129  dif1enlem  9157  unxpdomlem3  9231  fineqvlem  9239  infn0  9275  fodomfir  9300  f1opwfi  9326  fsuppcolem  9374  fsuppco  9375  mapfienlem1  9378  mapfienlem2  9379  supub  9432  suplub  9433  ordtypelem2  9494  ordtypelem3  9495  ordtypelem6  9498  ordtypelem7  9499  wemapso2lem  9527  wdom2d  9555  brwdom3  9557  ixpiunwdom  9565  inf3lem2  9611  inf3lem6  9615  oancom  9633  infdifsn  9639  cantnfp1lem3  9662  cantnflem3  9673  cantnflem4  9674  oef1o  9680  cnfcom3  9686  tctr  9720  frinsg  9736  tz9.12lem3  9774  scottex  9875  scottexOLD  9876  cardid2  9961  infxpenlem  10019  acni3  10053  cardaleph  10095  iscard3  10099  dfac5lem4  10132  dfac5lem5  10133  kmlem1  10156  cofsmo  10274  fin4en1  10314  enfin2i  10326  fin23lem28  10345  fin23lem38  10354  isf32lem6  10363  enfin1ai  10389  hsmexlem2  10432  hsmexlem4  10434  domtriomlem  10447  axdc2lem  10453  axdc3lem2  10456  ac6num  10484  zorn2lem2  10502  brdom3  10534  alephval2  10584  alephreg  10594  pwcfsdom  10595  smobeth  10598  fpwwe2lem5  10647  fpwwe2lem12  10654  canthp1lem2  10665  pwfseqlem3  10672  hargch  10685  winalim2  10708  gchina  10711  inar1  10787  0npi  10894  mulclpi  10905  mulcanpi  10912  nlt1pi  10918  nqereu  10941  prcdnq  11005  prnmax  11007  ltresr2  11153  axrnegex  11174  axpre-sup  11181  0nn0m1nnn0  12678  eluz2gt1  12972  1nuz2  12976  zsupss  12989  rpgt0  13057  ixxss1  13418  ixxss2  13419  ixxss12  13420  lbioo  13431  ubioo  13432  iccss2  13472  iccssico2  13475  elfzuz3  13577  serge0  14122  expge0  14164  expge1  14165  expaddzlem  14171  hashrabsn1  14440  hashfun  14504  ccatf1  14658  cshinj  14884  relexpuzrel  15127  shftfn  15148  01sqrexlem6  15336  rlimss  15591  lo1dm  15608  o1dm  15619  rlimrege0  15668  fsumf1o  15811  fsumge0  15884  incexc2  15929  supcvg  15947  fprodf1o  16037  divalglem9  16495  bitsfzolem  16528  bitsf1  16540  gcdcllem1  16593  bezout  16637  nprm  16782  dvdsprm  16798  coprm  16806  dfphi2  16869  phimullem  16874  phisum  16886  expnprm  16998  prmreclem2  17013  prmreclem5  17016  1arith  17023  4sqlem18  17058  vdwnnlem3  17093  ramtlecl  17096  rami  17111  0ram  17116  ramub1lem1  17122  prmgaplem5  17151  acsfiel  17746  isacs1i  17749  catlid  17775  catrid  17776  fullfo  18007  fthf1  18012  fthoppc  18018  invfuc  18070  prslem  18389  oduprs  18392  posi  18409  tleile  18511  resspos  18521  resstos  18522  dlatmjdi  18615  pslem  18664  tsrlin  18677  cnvtsr  18680  tsrdir  18696  mndid  18850  mhmf  18901  mhmlin  18905  mhm0  18906  mndind  18941  grpinvex  19071  grplinv  19117  mulgz  19229  mulgdirlem  19232  mulgdir  19233  mulgass  19238  nsgbi  19284  nmzbi  19291  ghmf  19351  ghmlin  19352  conjnsg  19385  gimf1o  19394  gagrpid  19425  gaf  19426  gaass  19428  psgnunilem5  19625  odid  19669  odf1o2  19704  gexid  19712  sylow1lem4  19732  pj1id  19830  efgredeu  19883  ablcmn  19918  cmncom  19929  mulgdi  19957  torsubg  19985  cyggenod2  20016  cygctb  20023  ghmcyg  20027  dprdf1o  20165  ablfacrplem  20198  ablfaclem2  20219  ablfac2  20222  simpg2nsg  20229  fincygsubgodexd  20246  ogrpinv0le  20267  ogrpsub  20268  ogrpaddlt  20269  crngmgp  20384  rnghmmgmhm  20588  rhmmhm  20625  rhmghm  20629  rimf1o  20644  nzrnz  20679  0ringbas  20693  subrgss  20738  subrg1cl  20746  rnghmsubcsetclem1  20797  zrinitorngc  20808  zrtermorngc  20809  rhmsubcsetclem1  20826  ringcinv  20837  zrtermoringc  20841  rrgeq0i  20865  domneq0  20874  domnrrg  20878  drngunit  20899  isdrng4  20906  fldcrngd  20909  drngmgp  20912  drngid  20913  drngdomn  20916  issubdrg  20950  fldhmsubc  20955  fldsdrgfld  20968  cntzsdrg  20972  abvge0  20987  srngcnv  21017  orngsqr  21036  ornglmulle  21037  orngrmulle  21038  ofldtos  21043  ofldlt1  21045  suborng  21046  subofld  21047  lmhmlin  21223  lmimf1o  21251  lvecdrng  21293  lspsolvlem  21333  islbs3  21346  lbsextlem3  21351  2idlelbas  21470  2idlcpblrng  21477  prmidl0  21545  qsidomlem1  21547  zringunit  21683  prmirredlem  21689  irinitoringc  21696  znidomb  21778  cygzn  21787  ofldchr  21793  psgndiflemB  21817  pjf  21930  frlmsslsp  22013  frlmlbs  22014  f1lindf  22039  lindsenlbs  22068  assalem  22076  psrbaglefi  22145  psrbagleadd1  22147  mplelsfi  22213  mplsubrglem  22222  mplcoe1  22257  mplbas2  22262  opsrtoslem2  22276  mhpmulcl  22381  psdmul  22398  coe1mul2  22499  matunitlindflem1  22905  matunitlindflem2  22906  matunitlindf  22907  pmatcoe1fsupp  22930  toponuni  23143  tpsuni  23165  mretopd  23321  neips  23342  neiptoptop  23360  neiptopnei  23361  perflp  23383  perfi  23384  cnf  23475  cnpf  23476  cnpimaex  23485  cnima  23494  t0sep  23553  t1ficld  23556  hausnei  23557  pnrmcld  23571  cnrmi  23589  cmpcov  23618  tgcmp  23630  hauscmplem  23635  connclo  23644  1stcclb  23673  2ndcdisj  23686  llyi  23704  nllyi  23705  ptpjpre1  23801  ptpjcn  23841  ptpjopn  23842  ptclsg  23845  dfac14  23848  txdis1cn  23865  pthaus  23868  hauseqlcld  23876  txkgen  23882  xkococn  23890  txconn  23919  hmeocnvcn  23991  fbssfi  24067  filss  24083  uffixfr  24153  flimneiss  24196  flimelbas  24198  flimfnfcls  24258  alexsubb  24276  alexsubALT  24281  ptcmplem2  24283  ptcmplem3  24284  ptcmplem4  24285  tmdgsum2  24326  ghmcnp  24345  tgpt0  24349  qustgplem  24351  istdrg2  24408  vscacn  24416  tvctdrg  24423  uspreg  24503  ucncn  24514  neipcfilu  24525  cuspcvg  24530  psmetxrge0  24543  isxmet2d  24557  prdsxmetlem  24598  imasdsf1olem  24603  xmstopn  24681  mstopn  24682  stdbdxmet  24745  prdsxmslem2  24759  nrgabv  24891  nmvs  24906  nvclvec  24927  nmoge0  24951  nghmcl  24957  nmoi  24958  nghmghm  24964  nmhmlmhm  24979  nmhmnghm  24980  icccmp  25056  xrge0gsumle  25064  metds0  25081  metdstri  25082  metdsre  25084  metdseq0  25085  metdscnlem  25086  metnrmlem1a  25089  icopnfcnv  25174  xrhmeo  25178  pcoval1  25245  cvslvec  25357  cvsunit  25363  recvs  25378  cphreccllem  25410  cphsscph  25483  cmetcvg  25517  lmle  25533  cmscmet  25578  cmetcusp1  25585  hlcph  25596  minveclem4  25664  ivthlem3  25685  ovolmge0  25709  ovolicc1  25748  ovolicc2lem3  25751  ovolicc2lem5  25753  dyadmbl  25832  i1ff  25908  i1frn  25909  i1fima2  25911  itg2monolem1  25982  dvnres  26163  c1liplem1  26228  c1lip2  26230  dvge0  26238  lhop1lem  26245  itgsubstlem  26280  fta1glem2  26399  fta1b  26402  idomrootle  26403  plyf  26428  plypf1  26442  plyadd  26447  plymul  26448  coeeu  26455  dgrlem  26459  coeid  26468  elqaalem3  26555  aareccl  26562  eff1olem  26786  relogf1o  26804  logdmn0  26878  logcnlem2  26881  logcnlem3  26882  efopnlem1  26894  efopnlem2  26895  logtayl2  26900  cxpcn3lem  26985  cxpcn3  26986  logbgcd1irr  27032  atandmneg  27144  atandmcj  27147  efiatan2  27155  cosatan  27159  cosatanne0  27160  dvatan  27173  areage0  27201  cxp2lim  27214  jensenlem2  27225  jensen  27226  eldmgm  27259  dmgmaddn0  27260  dmlogdmgm  27261  lgamgulmlem2  27267  lgamgulmlem3  27268  lgamgulmlem5  27270  lgambdd  27274  lgamucov  27275  ftalem3  27312  efnnfsumcl  27340  efchtdvds  27396  sqff1o  27419  fsumdvdsdiaglem  27420  dvdsppwf1o  27423  dvdsflf1o  27424  musum  27428  muinv  27430  mpodvdsmulf1o  27431  dvdsmulf1o  27433  lgsfle1  27543  lgsle1  27549  lgsdirprm  27568  lgsne0  27572  lgseisenlem3  27614  lgseisenlem4  27615  lgsquadlem1  27617  lgsquadlem2  27618  chebbnd1  27709  chtppilim  27712  chpchtlim  27716  chpo1ub  27717  dchrmusumlema  27730  dchrvmasumlem1  27732  dchrisum0lema  27751  dchrisum0lem2a  27754  logsqvma  27779  selberg3lem2  27795  pntrsumo1  27802  pnt2  27850  ostthlem1  27864  ostth3  27875  ltsval2  27893  leftlt  28119  rightgt  28120  precsexlem8  28480  precsexlem9  28481  precsexlem11  28483  elons2  28524  onleft  28526  ltonold  28527  oncutleft  28529  oncutlt  28530  zcuts0  28674  axtgcgrrflx  28804  axtgcgrid  28805  axtgsegcon  28806  axtg5seg  28807  axtgbtwnid  28808  axtgpasch  28809  axtgcont1  28810  tglng  28889  axcontlem7  29428  axcontlem10  29431  upgrle  29548  umgredg2  29558  lfgredgge2  29582  usgredg2ALT  29654  usgr1vr  29716  usgrexmpledg  29723  upgrres1  29774  fusgrvtxfi  29780  vtxnbuvtx  29852  cusgrcplgr  29881  vdumgr0  29941  vtxdgoddnumeven  30014  trlres  30163  pthhashvtx  30195  usgr2pth  30230  cyclispthon  30273  clwwlknlen  30503  clwwnonrepclwwnon  30826  2clwwlk2  30829  ablocom  31030  phpar2  31305  cbncms  31347  hlph  31371  hcaucvg  31668  hlimconvi  31673  shaddcl  31699  shmulcl  31700  chlimi  31716  chcompl  31724  choc1  31809  nmopre  32352  cnopc  32395  lnopl  32396  unop  32397  hmop  32404  cnfnc  32412  lnfnl  32413  nlelshi  32542  cnlnadjlem5  32553  elpjidm  32666  mdslle1i  32799  mdslle2i  32800  atcv0  32824  aciunf1lem  33137  padct  33191  ssnnssfz  33260  swrdrndisj  33399  ressprs  33408  pwrssmgc  33442  wrdpmtrlast  33535  cyc3evpm  33592  cycpmgcl  33595  cycpmconjslem2  33597  cyc3conja  33599  isarchi3  33629  archirng  33630  archirngz  33631  archiabllem1a  33633  archiabllem1b  33634  archiabllem2a  33636  archiabllem2c  33637  archiabllem2b  33638  archiabl  33640  isarchiofld  33641  elrgspnlem1  33684  elrgspnlem2  33685  elrgspnlem4  33687  elrgspnsubrun  33691  ricnzr1  33730  ricdomn1  33731  nn0omnd  33786  quslsm  33836  nsgmgclem  33842  nsgmgc  33843  mxidlirred  33877  krull  33883  ufdprmidl  33953  1arithufdlem4  33959  extvfvcl  34048  mplvrpmga  34057  sradrng  34094  extdg1id  34178  ply1annnr  34215  madjusmdetlem4  34342  qtophaus  34348  crefi  34359  cmpcref  34362  cmppcmp  34370  pcmplfin  34372  zart0  34391  tpr2rico  34424  rge0scvg  34461  zrhunitpreima  34488  qqhrhm  34501  esummono  34566  gsumesum  34571  esumrnmpt2  34580  esumpinfval  34585  esumpcvgval  34590  esumpmono  34591  0elsiga  34626  sigaclcu  34629  issgon  34635  inelpisys  34667  ldsysgenld  34673  ldgenpisyslem1  34676  sxuni  34706  isrnmeas  34713  measvuni  34727  measssd  34728  ddemeas  34749  imambfm  34775  elmbfmvol2  34780  dya2icoseg2  34791  omssubaddlem  34812  omssubadd  34813  carsgsigalem  34828  pmeasmono  34837  sibfinima  34852  oddpwdc  34867  oddpwdcv  34868  eulerpartlemf  34883  eulerpartlemt  34884  eulerpartlemr  34887  eulerpartlemgvv  34889  eulerpartlemgs2  34893  fiblem  34911  probtot  34925  ballotlem4  35012  ballotlem5  35013  ballotlemfrc  35040  ballotlemirc  35045  ballotth  35051  hgt750lemb  35166  bnj642  35260  bnj643  35261  bnj645  35262  bnj707  35267  bnj1379  35341  bnj1538  35366  bnj110  35369  bnj93  35374  bnj906  35441  bnj1006  35471  bnj1110  35493  bnj1121  35496  bnj1204  35523  bnj1321  35538  bnj1364  35539  bnj1398  35545  bnj1450  35561  bnj1312  35569  bnj1501  35578  bnj1523  35582  elscottrank  35630  elscottrankss  35632  tz9.1regs  35662  onvfowev  35715  subfacp1lem3  35763  subfacp1lem5  35765  pconncn  35805  connpconn  35816  cvmcov  35844  cvmliftlem1  35866  cvmliftlem10  35875  cvmlift2lem11  35894  cvmlift2lem12  35895  msubff1  36137  mvhf1  36140  mthmpps  36163  mclspps  36165  fundmpss  36348  funpartfun  36524  fnetg  36966  neibastop1  36980  filnetlem3  37001  onint1  37070  weiunlem  37084  weiunpo  37086  weiunse  37089  bj-nnfa  37463  bj-idres  37914  bj-rvecrr  38051  icorempo  38107  pibt2  38173  wl-nfeqfb  38301  phpreu  38360  fin2solem  38362  fin2so  38363  ptrest  38370  poimirlem1  38372  poimirlem2  38373  poimirlem3  38374  poimirlem4  38375  poimirlem5  38376  poimirlem6  38377  poimirlem7  38378  poimirlem8  38379  poimirlem9  38380  poimirlem10  38381  poimirlem11  38382  poimirlem12  38383  poimirlem13  38384  poimirlem14  38385  poimirlem15  38386  poimirlem16  38387  poimirlem17  38388  poimirlem18  38389  poimirlem19  38390  poimirlem20  38391  poimirlem21  38392  poimirlem22  38393  poimirlem23  38394  poimirlem24  38395  poimirlem26  38397  poimirlem27  38398  poimirlem29  38400  poimirlem31  38402  mblfinlem2  38409  dvtan  38421  itg2gt0cn  38426  ftc1anclem7  38450  ftc1anclem8  38451  ftc1anc  38452  cover2  38467  indexa  38485  istotbnd3  38523  sstotbnd2  38526  sstotbnd  38527  totbndss  38529  equivtotbnd  38530  isbnd3  38536  totbndbnd  38541  equivbnd  38542  prdsbnd  38545  prdstotbnd  38546  heibor  38573  zrdivrng  38705  crngocom  38753  isfld2  38757  dmncrng  38808  eqvrelrel  39431  disjrel  39580  disjdmqscossss  39656  prter2  39756  toycom  39848  lsateln0  39870  lpssat  39888  lssat  39891  oposlem  40057  olop  40089  omllaw  40118  cvlexch1  40203  dihpN  42211  mapdordlem2  42512  linvh  42964  idomnnzpownz  43000  idomnnzgmulnz  43001  aks6d1c5lem2  43006  deg1pow  43009  redvmptabs  43237  readvrec2  43238  readvrec  43239  mhphflem  43444  prjspertr  43453  nacsfg  43552  nacsfix  43559  mzpindd  43593  diophrw  43606  diophrex  43622  rexzrexnn0  43647  pell1234qrdich  43704  rmspecnonsq  43750  rmspecfund  43752  rmspecpos  43759  monotoddzzfi  43785  ltrmxnn0  43792  rmxnn  43794  jm2.23  43839  jm3.1lem2  43861  dnnumch3  43890  lnmlssfg  43923  lnmlmic  43931  lnrlnm  43956  lnr2i  43959  lpirlnr  43960  hbtlem6  43972  hbt  43973  mnccoe  43981  proot1mul  44037  proot1hash  44038  deg1mhm  44043  ondif1i  44105  limnsuc  44108  cantnfresb  44167  succlg  44171  ntrneifv2  44922  grucollcld  45086  mnurndlem1  45107  ismnushort  45127  radcnvrat  45140  binomcxplemdvbinom  45179  binomcxplemcvg  45180  binomcxplemnotnn0  45182  ordelordALT  45362  2uasbanh  45386  ordelordALTVD  45691  relprel  45776  elixpconstg  45923  rabidim2  45936  disjinfi  46026  supminfxr2  46299  sumnnodd  46462  stoweidlem7  46837  stoweidlem14  46844  stoweidlem16  46846  stoweidlem24  46854  stoweidlem31  46861  stoweidlem54  46884  wallispilem3  46897  fourierdlem42  46979  fourierdlem48  46984  fourierdlem51  46987  fourierdlem64  47000  fourierdlem76  47012  fourierdlem79  47015  fourierdlem81  47017  fourierdlem87  47023  etransclem28  47092  etransclem32  47096  sge0fodjrnlem  47246  hoidmvlelem3  47427  ovolval5lem3  47484  pimrecltpos  47538  pimrecltneg  47554  issmflem  47557  smfaddlem1  47593  smfsuplem1  47641  smfsuplem3  47643  smflimsuplem7  47656  smfliminflem  47660  chndin  47721  chnrin  47726  nfunsnafv  48032  faovcl  48090  tz6.12-2-afv2  48127  tz6.12i-afv2  48133  sprel  48386  evendiv2z  48550  oddp1div2z  48551  2dvdseven  48571  2ndvdsodd  48573  perfectALTVlem1  48639  sbgoldbm  48702  upgrimtrls  48824  upgrimpthslem1  48825  upgrimspths  48828  upgrimcycls  48829  uhgrimisgrgric  48849  gpgprismgr4cycllem2  49014  clintopcllaw  49128  uzlidlring  49152  rngccatidALTV  49189  funcringcsetcALTV2lem7  49213  ringccatidALTV  49223  ringcinvALTV  49227  funcringcsetclem7ALTV  49236  fldhmsubcALTV  49250  ssnn0ssfz  49281  el0ldepsnzr  49399  regt1loggt0  49468  elbigodm  49487  fllogbd  49492  rrx2xpref1o  49650  unilbss  49748  fdomne0  49780  f002  49784  xpco2  49787  imaf1homlem  50035  idemb  50087  uobeq2  50329  thincmo2  50354  thincmoALT  50357  fullthinc  50378  idfudiag1  50453  elsetrecslem  50627  dvsec  50691  dvcsc  50692  dvcot  50693  alseueu  50768