Theorem simprbi 499

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  simplbiim  507  xornan  1510  sb1ALT  2582  eumo  2663  reurmo  3433  pssne  4073  pssn2lp  4078  ssnpss  4080  eldifn  4104  elinel2  4173  rabsnt  4667  eldifsni  4722  unimax  4874  ssintub  4894  moop2  5392  pwssun  5456  weso  5546  opelxp2  5597  wfisg  6183  ordwe  6204  funmo  6371  funopg  6389  funun  6400  fununi  6429  fndm  6455  frn  6520  f1ss  6580  f1ssr  6581  forn  6593  f1f1orn  6626  f1orescnv  6630  f1imacnv  6631  funcocnv2  6639  dffv2  6756  exfo  6871  foelrn  6872  isorel  7079  isoini2  7092  f1ofveu  7151  fovcl  7279  onminesb  7513  onminsb  7514  tfis  7569  limomss  7585  nnlim  7593  ssnlim  7599  curry1  7799  curry2  7802  f1o2ndf1  7818  fnwelem  7825  mpoxopn0yelv  7879  wfrlem5  7959  tz7.48lem  8077  dif20el  8130  oeordi  8213  oeeulem  8227  oeeui  8228  nnawordex  8263  swoer  8319  eceqoveq  8402  mapsnconst  8456  resixpfo  8500  boxcutc  8505  sdomnen  8538  en0  8572  en1  8576  fodomr  8668  unxpdomlem3  8724  fineqvlem  8732  f1opwfi  8828  fsuppcolem  8864  fsuppco  8865  mapfienlem1  8868  mapfienlem2  8869  supub  8923  suplub  8924  ordtypelem2  8983  ordtypelem3  8984  ordtypelem6  8987  ordtypelem7  8988  wemapso2lem  9016  wdom2d  9044  brwdom3  9046  ixpiunwdom  9055  inf3lem2  9092  inf3lem6  9096  oancom  9114  infdifsn  9120  cantnfp1lem3  9143  cantnflem3  9154  cantnflem4  9155  oef1o  9161  cnfcom3  9167  tctr  9182  tz9.12lem3  9218  scottex  9314  cardid2  9382  infxpenlem  9439  acni3  9473  cardaleph  9515  iscard3  9519  dfac5lem4  9552  dfac5lem5  9553  kmlem1  9576  cofsmo  9691  fin4en1  9731  enfin2i  9743  fin23lem28  9762  fin23lem38  9771  isf32lem6  9780  enfin1ai  9806  hsmexlem2  9849  hsmexlem4  9851  domtriomlem  9864  axdc2lem  9870  axdc3lem2  9873  ac6num  9901  zorn2lem2  9919  brdom3  9950  alephval2  9994  alephreg  10004  pwcfsdom  10005  smobeth  10008  fpwwe2lem6  10057  fpwwe2lem13  10064  canthp1lem2  10075  pwfseqlem3  10082  hargch  10095  winalim2  10118  gchina  10121  inar1  10197  0npi  10304  mulclpi  10315  mulcanpi  10322  nlt1pi  10328  nqereu  10351  prcdnq  10415  prnmax  10417  ltresr2  10563  axrnegex  10584  axpre-sup  10591  eluz2gt1  12321  1nuz2  12325  zsupss  12338  rpgt0  12402  ixxss1  12757  ixxss2  12758  ixxss12  12759  lbioo  12770  ubioo  12771  iccss2  12808  iccssico2  12811  elfzuz3  12906  serge0  13425  expge0  13466  expge1  13467  expaddzlem  13473  hashrabsn1  13736  hashfun  13799  cshinj  14173  relexpuzrel  14411  shftfn  14432  sqrlem6  14607  rlimss  14859  lo1dm  14876  o1dm  14887  rlimrege0  14936  fsumf1o  15080  fsumge0  15150  incexc2  15193  supcvg  15211  fprodf1o  15300  divalglem9  15752  bitsfzolem  15783  bitsf1  15795  gcdcllem1  15848  bezout  15891  nprm  16032  dvdsprm  16047  coprm  16055  dfphi2  16111  phimullem  16116  phisum  16127  expnprm  16238  prmreclem2  16253  prmreclem5  16256  1arith  16263  4sqlem18  16298  vdwnnlem3  16333  ramtlecl  16336  rami  16351  0ram  16356  ramub1lem1  16362  prmgaplem5  16391  acsfiel  16925  isacs1i  16928  catlid  16954  catrid  16955  fullfo  17182  fthf1  17187  fthoppc  17193  invfuc  17244  prslem  17541  posi  17560  dlatmjdi  17804  pslem  17816  tsrlin  17829  cnvtsr  17832  tsrdir  17848  mndid  17921  mhmf  17961  mhmlin  17963  mhm0  17964  mndind  17992  grpinvex  18113  grplinv  18152  mulgz  18255  mulgdirlem  18258  mulgdir  18259  mulgass  18264  nsgbi  18309  nmzbi  18316  ghmf  18362  ghmlin  18363  conjnsg  18394  gimf1o  18403  gagrpid  18424  gaf  18425  gaass  18427  psgnunilem5  18622  odid  18666  odf1o2  18698  gexid  18706  sylow1lem4  18726  pj1id  18825  efgredeu  18878  ablcmn  18913  cmncom  18923  mulgdi  18947  torsubg  18974  cyggenod2  19004  cygctb  19012  ghmcyg  19016  dprdf1o  19154  ablfacrplem  19187  ablfaclem2  19208  ablfac2  19211  simpg2nsg  19218  fincygsubgodexd  19235  crngmgp  19305  rhmmhm  19474  rhmghm  19477  drngunit  19507  drngmgp  19514  drngid  19516  subrgss  19536  subrg1cl  19543  issubdrg  19560  cntzsdrg  19581  abvge0  19596  srngcnv  19624  lmhmlin  19807  lmimf1o  19835  lvecdrng  19877  lspsolvlem  19914  islbs3  19927  lbsextlem3  19932  2idlcpbl  20007  nzrnz  20033  opprnzr  20038  rrgeq0i  20062  domneq0  20070  domnrrg  20073  drngdomn  20076  fldidom  20078  assalem  20089  mplsubrglem  20219  mplcoe1  20246  mplbas2  20251  opsrtoslem2  20265  mplelsfi  20271  coe1mul2  20437  zringunit  20635  prmirredlem  20640  znidomb  20708  cygzn  20717  psgndiflemB  20744  pjf  20857  frlmsslsp  20940  frlmlbs  20941  f1lindf  20966  pmatcoe1fsupp  21309  toponuni  21522  tpsuni  21544  mretopd  21700  neips  21721  neiptoptop  21739  neiptopnei  21740  perflp  21762  perfi  21763  cnf  21854  cnpf  21855  cnpimaex  21864  cnima  21873  t0sep  21932  t1ficld  21935  hausnei  21936  pnrmcld  21950  cnrmi  21968  cmpcov  21997  tgcmp  22009  hauscmplem  22014  connclo  22023  1stcclb  22052  2ndcdisj  22064  llyi  22082  nllyi  22083  ptpjpre1  22179  ptpjcn  22219  ptpjopn  22220  ptclsg  22223  dfac14  22226  txdis1cn  22243  pthaus  22246  hauseqlcld  22254  txkgen  22260  xkococn  22268  txconn  22297  hmeocnvcn  22369  fbssfi  22445  filss  22461  uffixfr  22531  flimneiss  22574  flimelbas  22576  flimfnfcls  22636  alexsubb  22654  alexsubALT  22659  ptcmplem2  22661  ptcmplem3  22662  ptcmplem4  22663  tmdgsum2  22704  ghmcnp  22723  tgpt0  22727  qustgplem  22729  istdrg2  22786  vscacn  22794  tvctdrg  22801  uspreg  22883  ucncn  22894  neipcfilu  22905  cuspcvg  22910  psmetxrge0  22923  isxmet2d  22937  prdsxmetlem  22978  imasdsf1olem  22983  xmstopn  23061  mstopn  23062  stdbdxmet  23125  prdsxmslem2  23139  nrgabv  23270  nmvs  23285  nvclvec  23306  nmoge0  23330  nghmcl  23336  nmoi  23337  nghmghm  23343  nmhmlmhm  23358  nmhmnghm  23359  icccmp  23433  xrge0gsumle  23441  metds0  23458  metdstri  23459  metdsre  23461  metdseq0  23462  metdscnlem  23463  metnrmlem1a  23466  icopnfcnv  23546  xrhmeo  23550  pcoval1  23617  cvslvec  23729  cvsunit  23735  cphreccllem  23782  cphsscph  23854  cmetcvg  23888  lmle  23904  cmscmet  23949  cmetcusp1  23956  hlcph  23967  minveclem4  24035  ivthlem3  24054  ovolmge0  24078  ovolicc1  24117  ovolicc2lem3  24120  ovolicc2lem5  24122  dyadmbl  24201  i1ff  24277  i1frn  24278  i1fima2  24280  itg2monolem1  24351  dvnres  24528  c1liplem1  24593  c1lip2  24595  dvge0  24603  lhop1lem  24610  itgsubstlem  24645  fta1glem2  24760  fta1b  24763  plyf  24788  plypf1  24802  plyadd  24807  plymul  24808  coeeu  24815  dgrlem  24819  coeid  24828  elqaalem3  24910  aareccl  24915  eff1olem  25132  relogf1o  25150  logdmn0  25223  logcnlem2  25226  logcnlem3  25227  efopnlem1  25239  efopnlem2  25240  logtayl2  25245  cxpcn3lem  25328  cxpcn3  25329  logbgcd1irr  25372  atandmneg  25484  atandmcj  25487  efiatan2  25495  cosatan  25499  cosatanne0  25500  dvatan  25513  areage0  25541  cxp2lim  25554  jensenlem2  25565  jensen  25566  eldmgm  25599  dmgmaddn0  25600  dmlogdmgm  25601  lgamgulmlem2  25607  lgamgulmlem3  25608  lgamgulmlem5  25610  lgambdd  25614  lgamucov  25615  ftalem3  25652  efnnfsumcl  25680  efchtdvds  25736  sqff1o  25759  fsumdvdsdiaglem  25760  dvdsppwf1o  25763  dvdsflf1o  25764  musum  25768  muinv  25770  dvdsmulf1o  25771  lgsfle1  25882  lgsle1  25888  lgsdirprm  25907  lgsne0  25911  lgseisenlem3  25953  lgseisenlem4  25954  lgsquadlem1  25956  lgsquadlem2  25957  chebbnd1  26048  chtppilim  26051  chpchtlim  26055  chpo1ub  26056  dchrmusumlema  26069  dchrvmasumlem1  26071  dchrisum0lema  26090  dchrisum0lem2a  26093  logsqvma  26118  selberg3lem2  26134  pntrsumo1  26141  pnt2  26189  ostthlem1  26203  ostth3  26214  axtgcgrrflx  26248  axtgcgrid  26249  axtgsegcon  26250  axtg5seg  26251  axtgbtwnid  26252  axtgpasch  26253  axtgcont1  26254  tglng  26332  axcontlem7  26756  axcontlem10  26759  upgrle  26875  umgredg2  26885  lfgredgge2  26909  usgredg2ALT  26975  usgr1vr  27037  usgrexmpledg  27044  upgrres1  27095  fusgrvtxfi  27101  vtxnbuvtx  27173  cusgrcplgr  27202  vdumgr0  27262  vtxdgoddnumeven  27335  trlres  27482  usgr2pth  27545  cyclispthon  27582  clwwlknlen  27810  clwwnonrepclwwnon  28124  2clwwlk2  28127  ablocom  28325  phpar2  28600  cbncms  28642  hlph  28666  hcaucvg  28963  hlimconvi  28968  shaddcl  28994  shmulcl  28995  chlimi  29011  chcompl  29019  choc1  29104  nmopre  29647  cnopc  29690  lnopl  29691  unop  29692  hmop  29699  cnfnc  29707  lnfnl  29708  nlelshi  29837  cnlnadjlem5  29848  elpjidm  29961  mdslle1i  30094  mdslle2i  30095  atcv0  30119  chpssati  30140  fovcld  30385  aciunf1lem  30407  padct  30455  ssnnssfz  30510  ccatf1  30625  swrdrndisj  30631  ressprs  30642  oduprs  30643  resspos  30646  resstos  30647  tleile  30648  ogrpinv0le  30716  ogrpsub  30717  ogrpaddlt  30718  cyc3evpm  30792  cycpmgcl  30795  cycpmconjslem2  30797  cyc3conja  30799  isarchi3  30816  archirng  30817  archirngz  30818  archiabllem1a  30820  archiabllem1b  30821  archiabllem2a  30823  archiabllem2c  30824  archiabllem2b  30825  archiabl  30827  orngsqr  30877  ornglmulle  30878  orngrmulle  30879  ofldtos  30884  ofldlt1  30886  ofldchr  30887  suborng  30888  subofld  30889  isarchiofld  30890  nn0omnd  30914  qsidomlem1  30965  krull  30980  sradrng  30988  extdg1id  31053  madjusmdetlem4  31095  qtophaus  31100  crefi  31111  cmpcref  31114  cmppcmp  31122  pcmplfin  31124  tpr2rico  31155  rge0scvg  31192  zrhunitpreima  31219  qqhrhm  31230  esummono  31313  gsumesum  31318  esumrnmpt2  31327  esumpinfval  31332  esumpcvgval  31337  esumpmono  31338  0elsiga  31373  sigaclcu  31376  issgon  31382  inelpisys  31413  ldsysgenld  31419  ldgenpisyslem1  31422  sxuni  31452  isrnmeas  31459  measvuni  31473  measssd  31474  ddemeas  31495  imambfm  31520  elmbfmvol2  31525  dya2icoseg2  31536  omssubaddlem  31557  omssubadd  31558  carsgsigalem  31573  pmeasmono  31582  sibfinima  31597  oddpwdc  31612  oddpwdcv  31613  eulerpartlemf  31628  eulerpartlemt  31629  eulerpartlemr  31632  eulerpartlemgvv  31634  eulerpartlemgs2  31638  fiblem  31656  probtot  31670  ballotlem4  31756  ballotlem5  31757  ballotlemfrc  31784  ballotlemirc  31789  ballotth  31795  hgt750lemb  31927  bnj642  32019  bnj643  32020  bnj645  32021  bnj707  32026  bnj1379  32102  bnj1538  32127  bnj110  32130  bnj93  32135  bnj906  32202  bnj1006  32232  bnj1110  32254  bnj1121  32257  bnj1204  32284  bnj1321  32299  bnj1364  32300  bnj1398  32306  bnj1450  32322  bnj1312  32330  bnj1501  32339  bnj1523  32343  0nn0m1nnn0  32351  subfacp1lem3  32429  subfacp1lem5  32431  pconncn  32471  connpconn  32482  cvmcov  32510  cvmliftlem1  32532  cvmliftlem10  32541  cvmlift2lem11  32560  cvmlift2lem12  32561  msubff1  32803  mvhf1  32806  mthmpps  32829  mclspps  32831  fundmpss  33009  tfisg  33055  frpoinsg  33081  frinsg  33087  sltval2  33163  funpartfun  33404  fnetg  33693  neibastop1  33707  filnetlem3  33728  onint1  33797  bj-nnfa  34060  bj-idres  34455  bj-rvecrr  34581  icorempo  34635  pibt2  34701  wl-nfeqfb  34791  phpreu  34891  fin2solem  34893  fin2so  34894  lindsenlbs  34902  matunitlindflem1  34903  matunitlindflem2  34904  matunitlindf  34905  ptrest  34906  poimirlem1  34908  poimirlem2  34909  poimirlem3  34910  poimirlem4  34911  poimirlem5  34912  poimirlem6  34913  poimirlem7  34914  poimirlem8  34915  poimirlem9  34916  poimirlem10  34917  poimirlem11  34918  poimirlem12  34919  poimirlem13  34920  poimirlem14  34921  poimirlem15  34922  poimirlem16  34923  poimirlem17  34924  poimirlem18  34925  poimirlem19  34926  poimirlem20  34927  poimirlem21  34928  poimirlem22  34929  poimirlem23  34930  poimirlem24  34931  poimirlem26  34933  poimirlem27  34934  poimirlem29  34936  poimirlem31  34938  mblfinlem2  34945  dvtan  34957  itg2gt0cn  34962  ftc1anclem7  34988  ftc1anclem8  34989  ftc1anc  34990  cover2  35004  indexa  35023  istotbnd3  35064  sstotbnd2  35067  sstotbnd  35068  totbndss  35070  equivtotbnd  35071  isbnd3  35077  totbndbnd  35082  equivbnd  35083  prdsbnd  35086  prdstotbnd  35087  heibor  35114  zrdivrng  35246  crngocom  35294  isfld2  35298  dmncrng  35349  eqvrelrel  35847  disjrel  35978  prter2  36032  toycom  36124  lsateln0  36146  lpssat  36164  lssat  36167  oposlem  36333  olop  36365  omllaw  36394  cvlexch1  36479  dihpN  38487  mapdordlem2  38788  prjspertr  39275  nacsfg  39322  nacsfix  39329  mzpindd  39363  diophrw  39376  diophrex  39392  rexzrexnn0  39421  pell1234qrdich  39478  rmspecnonsq  39524  rmspecfund  39526  rmspecpos  39533  monotoddzzfi  39559  ltrmxnn0  39566  rmxnn  39568  jm2.23  39613  jm3.1lem2  39635  dnnumch3  39667  lnmlssfg  39700  lnmlmic  39708  lnrlnm  39733  lnr2i  39736  lpirlnr  39737  hbtlem6  39749  hbt  39750  mnccoe  39758  idomrootle  39815  proot1mul  39819  proot1hash  39820  deg1mhm  39827  ntrneifv2  40450  grucollcld  40616  mnurndlem1  40637  radcnvrat  40666  binomcxplemdvbinom  40705  binomcxplemcvg  40706  binomcxplemnotnn0  40708  ordelordALT  40891  2uasbanh  40915  ordelordALTVD  41221  elixpconstg  41375  rabidim2  41388  foelrnf  41467  disjinfi  41474  supminfxr2  41765  sumnnodd  41931  stoweidlem7  42312  stoweidlem14  42319  stoweidlem16  42321  stoweidlem24  42329  stoweidlem31  42336  stoweidlem54  42359  wallispilem3  42372  fourierdlem42  42454  fourierdlem48  42459  fourierdlem51  42462  fourierdlem64  42475  fourierdlem76  42487  fourierdlem79  42490  fourierdlem81  42492  fourierdlem87  42498  etransclem28  42567  etransclem32  42571  sge0fodjrnlem  42718  hoidmvlelem3  42899  pimrecltpos  43007  pimrecltneg  43021  issmflem  43024  smfaddlem1  43059  smfsuplem1  43105  smfsuplem3  43107  smflimsuplem7  43120  smfliminflem  43124  nfunsnafv  43361  faovcl  43419  tz6.12-2-afv2  43456  tz6.12i-afv2  43462  sprel  43666  evendiv2z  43817  oddp1div2z  43818  2dvdseven  43838  2ndvdsodd  43840  perfectALTVlem1  43906  sbgoldbm  43969  clintopcllaw  44138  0ringbas  44162  rnghmmgmhm  44185  uzlidlring  44220  rnghmsubcsetclem1  44266  rngccatidALTV  44280  zrinitorngc  44291  zrtermorngc  44292  rhmsubcsetclem1  44312  funcringcsetcALTV2lem7  44333  ringccatidALTV  44343  funcringcsetclem7ALTV  44356  irinitoringc  44360  zrtermoringc  44361  fldhmsubc  44375  fldhmsubcALTV  44393  ssnn0ssfz  44417  el0ldepsnzr  44542  regt1loggt0  44616  elbigodm  44635  fllogbd  44640  rrx2xpref1o  44725  elsetrecslem  44821