Theorem simprbi 500

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  511  xornan  1533  just2-df  2081  eumo  2599  reurmo  3364  pssne  4047  pssn2lp  4053  ssnpss  4055  eldifn  4080  elinel2  4149  rabsnt  4684  eldifsni  4744  unimax  4897  ssintub  4918  moop2  5465  pwssun  5532  weso  5631  opelxp2  5683  predpo  6299  frpoinsg  6319  ordwe  6348  funmo  6526  funopg  6544  funun  6556  fununi  6585  funimaexg  6597  fndm  6613  frn  6688  f1ss  6756  f1ssr  6757  forn  6770  f1f1orn  6807  f1orescnv  6811  f1imacnv  6812  funcocnv2  6821  dffv2  6951  exfo  7075  foelrn  7077  foelrnf  7078  isorel  7299  isoini2  7312  f1ofveu  7379  fovcld  7512  onminesb  7765  onminsb  7766  tfisg  7823  tfis  7824  limomss  7840  nnlim  7849  ssnlim  7855  resf1ext2b  7905  curry1  8071  curry2  8074  f1o2ndf1  8089  fnwelem  8099  mpoxopn0yelv  8181  tz7.48lem  8400  dif20el  8462  oeordi  8545  oeeulem  8559  oeeui  8560  nnawordex  8595  swoer  8698  eceqoveq  8792  mapsnconst  8863  resixpfo  8907  boxcutc  8912  sdomnen  8951  en0  8988  en0ALT  8989  en0r  8990  en1  8994  dom0  9066  fodomr  9089  dif1enlem  9117  unxpdomlem3  9191  fineqvlem  9199  infn0  9235  fodomfir  9261  f1opwfi  9289  fsuppcolem  9337  fsuppco  9338  mapfienlem1  9341  mapfienlem2  9342  supub  9395  suplub  9396  ordtypelem2  9457  ordtypelem3  9458  ordtypelem6  9461  ordtypelem7  9462  wemapso2lem  9490  wdom2d  9518  brwdom3  9520  ixpiunwdom  9528  inf3lem2  9574  inf3lem6  9578  oancom  9596  infdifsn  9602  cantnfp1lem3  9625  cantnflem3  9636  cantnflem4  9637  oef1o  9643  cnfcom3  9649  tctr  9683  frinsg  9699  tz9.12lem3  9737  scottex  9833  cardid2  9901  infxpenlem  9959  acni3  9993  cardaleph  10035  iscard3  10039  dfac5lem4  10072  dfac5lem5  10073  dfac5lem4OLD  10074  kmlem1  10097  cofsmo  10216  fin4en1  10256  enfin2i  10268  fin23lem28  10287  fin23lem38  10296  isf32lem6  10305  enfin1ai  10331  hsmexlem2  10374  hsmexlem4  10376  domtriomlem  10389  axdc2lem  10395  axdc3lem2  10398  ac6num  10426  zorn2lem2  10444  brdom3  10475  alephval2  10520  alephreg  10530  pwcfsdom  10531  smobeth  10534  fpwwe2lem5  10583  fpwwe2lem12  10590  canthp1lem2  10601  pwfseqlem3  10608  hargch  10621  winalim2  10644  gchina  10647  inar1  10723  0npi  10830  mulclpi  10841  mulcanpi  10848  nlt1pi  10854  nqereu  10877  prcdnq  10941  prnmax  10943  ltresr2  11089  axrnegex  11110  axpre-sup  11117  eluz2gt1  12911  1nuz2  12915  zsupss  12928  rpgt0  12996  ixxss1  13357  ixxss2  13358  ixxss12  13359  lbioo  13370  ubioo  13371  iccss2  13411  iccssico2  13414  elfzuz3  13516  serge0  14059  expge0  14101  expge1  14102  expaddzlem  14108  hashrabsn1  14377  hashfun  14440  cshinj  14814  relexpuzrel  15055  shftfn  15076  01sqrexlem6  15250  rlimss  15505  lo1dm  15522  o1dm  15533  rlimrege0  15582  fsumf1o  15726  fsumge0  15799  incexc2  15844  supcvg  15862  fprodf1o  15952  divalglem9  16411  bitsfzolem  16444  bitsf1  16456  gcdcllem1  16509  bezout  16553  nprm  16698  dvdsprm  16714  coprm  16722  dfphi2  16785  phimullem  16790  phisum  16802  expnprm  16914  prmreclem2  16929  prmreclem5  16932  1arith  16939  4sqlem18  16974  vdwnnlem3  17009  ramtlecl  17012  rami  17027  0ram  17032  ramub1lem1  17038  prmgaplem5  17067  acsfiel  17662  isacs1i  17665  catlid  17691  catrid  17692  fullfo  17923  fthf1  17928  fthoppc  17934  invfuc  17986  prslem  18305  oduprs  18308  posi  18325  tleile  18427  resspos  18437  resstos  18438  dlatmjdi  18531  pslem  18580  tsrlin  18593  cnvtsr  18596  tsrdir  18612  mndid  18754  mhmf  18799  mhmlin  18803  mhm0  18804  mndind  18838  grpinvex  18961  grplinv  19007  mulgz  19120  mulgdirlem  19123  mulgdir  19124  mulgass  19129  nsgbi  19174  nmzbi  19181  ghmf  19236  ghmlin  19237  conjnsg  19270  gimf1o  19279  gagrpid  19310  gaf  19311  gaass  19313  psgnunilem5  19510  odid  19554  odf1o2  19589  gexid  19597  sylow1lem4  19617  pj1id  19715  efgredeu  19768  ablcmn  19803  cmncom  19814  mulgdi  19842  torsubg  19870  cyggenod2  19901  cygctb  19908  ghmcyg  19912  dprdf1o  20050  ablfacrplem  20083  ablfaclem2  20104  ablfac2  20107  simpg2nsg  20114  fincygsubgodexd  20131  ogrpinv0le  20152  ogrpsub  20153  ogrpaddlt  20154  crngmgp  20263  rnghmmgmhm  20464  rhmmhm  20500  rhmghm  20504  rimf1o  20514  nzrnz  20537  0ringbas  20550  subrgss  20594  subrg1cl  20602  rnghmsubcsetclem1  20653  zrinitorngc  20664  zrtermorngc  20665  rhmsubcsetclem1  20682  ringcinv  20693  zrtermoringc  20697  rrgeq0i  20721  domneq0  20730  domnrrg  20735  drngunit  20756  fldcrngd  20764  drngmgp  20767  drngid  20768  drngdomn  20771  issubdrg  20802  fldhmsubc  20807  fldsdrgfld  20820  cntzsdrg  20824  abvge0  20839  srngcnv  20869  orngsqr  20888  ornglmulle  20889  orngrmulle  20890  ofldtos  20895  ofldlt1  20897  suborng  20898  subofld  20899  lmhmlin  21075  lmimf1o  21103  lvecdrng  21145  lspsolvlem  21185  islbs3  21198  lbsextlem3  21203  2idlelbas  21307  2idlcpblrng  21314  zringunit  21491  prmirredlem  21497  irinitoringc  21504  znidomb  21586  cygzn  21595  ofldchr  21601  psgndiflemB  21625  pjf  21738  frlmsslsp  21821  frlmlbs  21822  f1lindf  21847  assalem  21882  psrbaglefi  21951  psrbagleadd1  21953  mplelsfi  22019  mplsubrglem  22028  mplcoe1  22063  mplbas2  22068  opsrtoslem2  22082  mhpmulcl  22187  psdmul  22204  coe1mul2  22305  pmatcoe1fsupp  22734  toponuni  22947  tpsuni  22969  mretopd  23125  neips  23146  neiptoptop  23164  neiptopnei  23165  perflp  23187  perfi  23188  cnf  23279  cnpf  23280  cnpimaex  23289  cnima  23298  t0sep  23357  t1ficld  23360  hausnei  23361  pnrmcld  23375  cnrmi  23393  cmpcov  23422  tgcmp  23434  hauscmplem  23439  connclo  23448  1stcclb  23477  2ndcdisj  23489  llyi  23507  nllyi  23508  ptpjpre1  23604  ptpjcn  23644  ptpjopn  23645  ptclsg  23648  dfac14  23651  txdis1cn  23668  pthaus  23671  hauseqlcld  23679  txkgen  23685  xkococn  23693  txconn  23722  hmeocnvcn  23794  fbssfi  23870  filss  23886  uffixfr  23956  flimneiss  23999  flimelbas  24001  flimfnfcls  24061  alexsubb  24079  alexsubALT  24084  ptcmplem2  24086  ptcmplem3  24087  ptcmplem4  24088  tmdgsum2  24129  ghmcnp  24148  tgpt0  24152  qustgplem  24154  istdrg2  24211  vscacn  24219  tvctdrg  24226  uspreg  24306  ucncn  24317  neipcfilu  24328  cuspcvg  24333  psmetxrge0  24346  isxmet2d  24360  prdsxmetlem  24401  imasdsf1olem  24406  xmstopn  24484  mstopn  24485  stdbdxmet  24548  prdsxmslem2  24562  nrgabv  24694  nmvs  24709  nvclvec  24730  nmoge0  24754  nghmcl  24760  nmoi  24761  nghmghm  24767  nmhmlmhm  24782  nmhmnghm  24783  icccmp  24859  xrge0gsumle  24867  metds0  24884  metdstri  24885  metdsre  24887  metdseq0  24888  metdscnlem  24889  metnrmlem1a  24892  icopnfcnv  24977  xrhmeo  24981  pcoval1  25048  cvslvec  25160  cvsunit  25166  recvs  25181  cphreccllem  25213  cphsscph  25286  cmetcvg  25320  lmle  25336  cmscmet  25381  cmetcusp1  25388  hlcph  25399  minveclem4  25467  ivthlem3  25488  ovolmge0  25512  ovolicc1  25551  ovolicc2lem3  25554  ovolicc2lem5  25556  dyadmbl  25635  i1ff  25711  i1frn  25712  i1fima2  25714  itg2monolem1  25785  dvnres  25966  c1liplem1  26031  c1lip2  26033  dvge0  26041  lhop1lem  26048  itgsubstlem  26083  fta1glem2  26202  fta1b  26205  idomrootle  26206  plyf  26231  plypf1  26245  plyadd  26250  plymul  26251  coeeu  26258  dgrlem  26262  coeid  26271  elqaalem3  26355  aareccl  26360  eff1olem  26583  relogf1o  26601  logdmn0  26675  logcnlem2  26678  logcnlem3  26679  efopnlem1  26691  efopnlem2  26692  logtayl2  26697  cxpcn3lem  26782  cxpcn3  26783  logbgcd1irr  26829  atandmneg  26941  atandmcj  26944  efiatan2  26952  cosatan  26956  cosatanne0  26957  dvatan  26970  areage0  26998  cxp2lim  27011  jensenlem2  27022  jensen  27023  eldmgm  27056  dmgmaddn0  27057  dmlogdmgm  27058  lgamgulmlem2  27064  lgamgulmlem3  27065  lgamgulmlem5  27067  lgambdd  27071  lgamucov  27072  ftalem3  27109  efnnfsumcl  27137  efchtdvds  27193  sqff1o  27216  fsumdvdsdiaglem  27217  dvdsppwf1o  27220  dvdsflf1o  27221  musum  27225  muinv  27227  mpodvdsmulf1o  27228  dvdsmulf1o  27230  lgsfle1  27340  lgsle1  27346  lgsdirprm  27365  lgsne0  27369  lgseisenlem3  27411  lgseisenlem4  27412  lgsquadlem1  27414  lgsquadlem2  27415  chebbnd1  27506  chtppilim  27509  chpchtlim  27513  chpo1ub  27514  dchrmusumlema  27527  dchrvmasumlem1  27529  dchrisum0lema  27548  dchrisum0lem2a  27551  logsqvma  27576  selberg3lem2  27592  pntrsumo1  27599  pnt2  27647  ostthlem1  27661  ostth3  27672  ltsval2  27690  leftlt  27916  rightgt  27917  precsexlem8  28277  precsexlem9  28278  precsexlem11  28280  elons2  28321  onleft  28323  ltonold  28324  oncutleft  28326  oncutlt  28327  zcuts0  28471  axtgcgrrflx  28601  axtgcgrid  28602  axtgsegcon  28603  axtg5seg  28604  axtgbtwnid  28605  axtgpasch  28606  axtgcont1  28607  tglng  28685  axcontlem7  29110  axcontlem10  29113  upgrle  29230  umgredg2  29240  lfgredgge2  29264  usgredg2ALT  29333  usgr1vr  29395  usgrexmpledg  29402  upgrres1  29453  fusgrvtxfi  29459  vtxnbuvtx  29531  cusgrcplgr  29560  vdumgr0  29620  vtxdgoddnumeven  29693  trlres  29838  usgr2pth  29903  cyclispthon  29943  clwwlknlen  30173  clwwnonrepclwwnon  30486  2clwwlk2  30489  ablocom  30690  phpar2  30965  cbncms  31007  hlph  31031  hcaucvg  31328  hlimconvi  31333  shaddcl  31359  shmulcl  31360  chlimi  31376  chcompl  31384  choc1  31469  nmopre  32012  cnopc  32055  lnopl  32056  unop  32057  hmop  32064  cnfnc  32072  lnfnl  32073  nlelshi  32202  cnlnadjlem5  32213  elpjidm  32326  mdslle1i  32459  mdslle2i  32460  atcv0  32484  aciunf1lem  32807  padct  32863  ssnnssfz  32932  ccatf1  33081  swrdrndisj  33089  ressprs  33098  pwrssmgc  33132  wrdpmtrlast  33227  cyc3evpm  33284  cycpmgcl  33287  cycpmconjslem2  33289  cyc3conja  33291  isarchi3  33321  archirng  33322  archirngz  33323  archiabllem1a  33325  archiabllem1b  33326  archiabllem2a  33328  archiabllem2c  33329  archiabllem2b  33330  archiabl  33332  isarchiofld  33333  elrgspnlem1  33377  elrgspnlem2  33378  elrgspnlem4  33380  elrgspnsubrun  33384  ricnzr1  33426  ricdomn1  33427  isdrng4  33436  nn0omnd  33484  quslsm  33545  nsgmgclem  33551  nsgmgc  33552  prmidl0  33591  qsidomlem1  33593  mxidlirred  33614  krull  33621  ufdprmidl  33691  1arithufdlem4  33697  extvfvcl  33787  mplvrpmlem  33794  mplvrpmga  33796  sradrng  33833  extdg1id  33917  ply1annnr  33954  madjusmdetlem4  34081  qtophaus  34087  crefi  34098  cmpcref  34101  cmppcmp  34109  pcmplfin  34111  zart0  34130  tpr2rico  34163  rge0scvg  34200  zrhunitpreima  34227  qqhrhm  34240  esummono  34305  gsumesum  34310  esumrnmpt2  34319  esumpinfval  34324  esumpcvgval  34329  esumpmono  34330  0elsiga  34365  sigaclcu  34368  issgon  34374  inelpisys  34405  ldsysgenld  34411  ldgenpisyslem1  34414  sxuni  34444  isrnmeas  34451  measvuni  34465  measssd  34466  ddemeas  34487  imambfm  34513  elmbfmvol2  34518  dya2icoseg2  34529  omssubaddlem  34550  omssubadd  34551  carsgsigalem  34566  pmeasmono  34575  sibfinima  34590  oddpwdc  34605  oddpwdcv  34606  eulerpartlemf  34621  eulerpartlemt  34622  eulerpartlemr  34625  eulerpartlemgvv  34627  eulerpartlemgs2  34631  fiblem  34649  probtot  34663  ballotlem4  34750  ballotlem5  34751  ballotlemfrc  34778  ballotlemirc  34783  ballotth  34789  hgt750lemb  34907  bnj642  35001  bnj643  35002  bnj645  35003  bnj707  35008  bnj1379  35082  bnj1538  35107  bnj110  35110  bnj93  35115  bnj906  35182  bnj1006  35212  bnj1110  35234  bnj1121  35237  bnj1204  35264  bnj1321  35279  bnj1364  35280  bnj1398  35286  bnj1450  35302  bnj1312  35310  bnj1501  35319  bnj1523  35323  tz9.1regs  35385  0nn0m1nnn0  35411  subfacp1lem3  35480  subfacp1lem5  35482  pconncn  35522  connpconn  35533  cvmcov  35561  cvmliftlem1  35583  cvmliftlem10  35592  cvmlift2lem11  35611  cvmlift2lem12  35612  msubff1  35854  mvhf1  35857  mthmpps  35880  mclspps  35882  fundmpss  36065  funpartfun  36241  fnetg  36653  neibastop1  36667  filnetlem3  36688  onint1  36757  weiunlem  36771  weiunpo  36773  weiunse  36776  bj-nnfa  37151  bj-idres  37600  bj-rvecrr  37737  icorempo  37793  pibt2  37859  wl-nfeqfb  37987  phpreu  38051  fin2solem  38053  fin2so  38054  lindsenlbs  38062  matunitlindflem1  38063  matunitlindflem2  38064  matunitlindf  38065  ptrest  38066  poimirlem1  38068  poimirlem2  38069  poimirlem3  38070  poimirlem4  38071  poimirlem5  38072  poimirlem6  38073  poimirlem7  38074  poimirlem8  38075  poimirlem9  38076  poimirlem10  38077  poimirlem11  38078  poimirlem12  38079  poimirlem13  38080  poimirlem14  38081  poimirlem15  38082  poimirlem16  38083  poimirlem17  38084  poimirlem18  38085  poimirlem19  38086  poimirlem20  38087  poimirlem21  38088  poimirlem22  38089  poimirlem23  38090  poimirlem24  38091  poimirlem26  38093  poimirlem27  38094  poimirlem29  38096  poimirlem31  38098  mblfinlem2  38105  dvtan  38117  itg2gt0cn  38122  ftc1anclem7  38146  ftc1anclem8  38147  ftc1anc  38148  cover2  38162  indexa  38180  istotbnd3  38218  sstotbnd2  38221  sstotbnd  38222  totbndss  38224  equivtotbnd  38225  isbnd3  38231  totbndbnd  38236  equivbnd  38237  prdsbnd  38240  prdstotbnd  38241  heibor  38268  zrdivrng  38400  crngocom  38448  isfld2  38452  dmncrng  38503  eqvrelrel  39128  disjrel  39277  disjdmqscossss  39353  prter2  39453  toycom  39545  lsateln0  39567  lpssat  39585  lssat  39588  oposlem  39754  olop  39786  omllaw  39815  cvlexch1  39900  dihpN  41908  mapdordlem2  42209  linvh  42661  idomnnzpownz  42697  idomnnzgmulnz  42698  aks6d1c5lem2  42703  deg1pow  42706  redvmptabs  42917  readvrec2  42918  readvrec  42919  mhphflem  43126  prjspertr  43135  nacsfg  43234  nacsfix  43241  mzpindd  43275  diophrw  43288  diophrex  43304  rexzrexnn0  43329  pell1234qrdich  43386  rmspecnonsq  43432  rmspecfund  43434  rmspecpos  43441  monotoddzzfi  43467  ltrmxnn0  43474  rmxnn  43476  jm2.23  43521  jm3.1lem2  43543  dnnumch3  43572  lnmlssfg  43605  lnmlmic  43613  lnrlnm  43638  lnr2i  43641  lpirlnr  43642  hbtlem6  43654  hbt  43655  mnccoe  43663  proot1mul  43719  proot1hash  43720  deg1mhm  43725  ondif1i  43787  limnsuc  43790  cantnfresb  43849  succlg  43853  ntrneifv2  44604  grucollcld  44784  mnurndlem1  44805  ismnushort  44825  radcnvrat  44838  binomcxplemdvbinom  44877  binomcxplemcvg  44878  binomcxplemnotnn0  44880  ordelordALT  45061  2uasbanh  45085  ordelordALTVD  45390  relprel  45475  elixpconstg  45615  rabidim2  45628  disjinfi  45718  supminfxr2  45991  sumnnodd  46154  stoweidlem7  46529  stoweidlem14  46536  stoweidlem16  46538  stoweidlem24  46546  stoweidlem31  46553  stoweidlem54  46576  wallispilem3  46589  fourierdlem42  46671  fourierdlem48  46676  fourierdlem51  46679  fourierdlem64  46692  fourierdlem76  46704  fourierdlem79  46707  fourierdlem81  46709  fourierdlem87  46715  etransclem28  46784  etransclem32  46788  sge0fodjrnlem  46938  hoidmvlelem3  47119  ovolval5lem3  47176  pimrecltpos  47230  pimrecltneg  47246  issmflem  47249  smfaddlem1  47285  smfsuplem1  47333  smfsuplem3  47335  smflimsuplem7  47348  smfliminflem  47352  nfunsnafv  47684  faovcl  47742  tz6.12-2-afv2  47779  tz6.12i-afv2  47785  sprel  48038  evendiv2z  48202  oddp1div2z  48203  2dvdseven  48223  2ndvdsodd  48225  perfectALTVlem1  48291  sbgoldbm  48354  upgrimtrls  48476  upgrimpthslem1  48477  upgrimspths  48480  upgrimcycls  48481  uhgrimisgrgric  48501  gpgprismgr4cycllem2  48666  clintopcllaw  48781  uzlidlring  48805  rngccatidALTV  48842  funcringcsetcALTV2lem7  48866  ringccatidALTV  48876  ringcinvALTV  48880  funcringcsetclem7ALTV  48889  fldhmsubcALTV  48903  ssnn0ssfz  48919  el0ldepsnzr  49037  regt1loggt0  49106  elbigodm  49125  fllogbd  49130  rrx2xpref1o  49288  unilbss  49387  fdomne0  49419  f002  49423  xpco2  49426  imaf1homlem  49676  idemb  49728  uobeq2  49970  thincmo2  49995  thincmoALT  49998  fullthinc  50019  idfudiag1  50094  elsetrecslem  50268