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  3355  pssne  4053  pssn2lp  4058  ssnpss  4060  eldifn  4086  elinel2  4156  rabsnt  4690  eldifsni  4748  unimax  4902  ssintub  4923  moop2  5458  pwssun  5524  weso  5623  opelxp2  5675  predpo  6289  frpoinsg  6309  ordwe  6338  funmo  6516  funopg  6534  funun  6546  fununi  6575  funimaexg  6587  fndm  6603  frn  6677  f1ss  6743  f1ssr  6744  forn  6757  f1f1orn  6793  f1orescnv  6797  f1imacnv  6798  funcocnv2  6807  dffv2  6937  exfo  7059  foelrn  7061  foelrnf  7062  isorel  7282  isoini2  7295  f1ofveu  7362  fovcld  7495  onminesb  7748  onminsb  7749  tfisg  7806  tfis  7807  limomss  7823  nnlim  7832  ssnlim  7838  resf1ext2b  7887  curry1  8056  curry2  8059  f1o2ndf1  8074  fnwelem  8083  mpoxopn0yelv  8165  tz7.48lem  8382  dif20el  8442  oeordi  8525  oeeulem  8539  oeeui  8540  nnawordex  8575  swoer  8677  eceqoveq  8771  mapsnconst  8842  resixpfo  8886  boxcutc  8891  sdomnen  8930  en0  8967  en0ALT  8968  en0r  8969  en1  8973  dom0  9045  fodomr  9068  dif1enlem  9096  unxpdomlem3  9170  fineqvlem  9178  infn0  9214  fodomfir  9240  f1opwfi  9268  fsuppcolem  9316  fsuppco  9317  mapfienlem1  9320  mapfienlem2  9321  supub  9374  suplub  9375  ordtypelem2  9436  ordtypelem3  9437  ordtypelem6  9440  ordtypelem7  9441  wemapso2lem  9469  wdom2d  9497  brwdom3  9499  ixpiunwdom  9507  inf3lem2  9550  inf3lem6  9554  oancom  9572  infdifsn  9578  cantnfp1lem3  9601  cantnflem3  9612  cantnflem4  9613  oef1o  9619  cnfcom3  9625  tctr  9659  frinsg  9675  tz9.12lem3  9713  scottex  9809  cardid2  9877  infxpenlem  9935  acni3  9969  cardaleph  10011  iscard3  10015  dfac5lem4  10048  dfac5lem5  10049  dfac5lem4OLD  10050  kmlem1  10073  cofsmo  10191  fin4en1  10231  enfin2i  10243  fin23lem28  10262  fin23lem38  10271  isf32lem6  10280  enfin1ai  10306  hsmexlem2  10349  hsmexlem4  10351  domtriomlem  10364  axdc2lem  10370  axdc3lem2  10373  ac6num  10401  zorn2lem2  10419  brdom3  10450  alephval2  10495  alephreg  10505  pwcfsdom  10506  smobeth  10509  fpwwe2lem5  10558  fpwwe2lem12  10565  canthp1lem2  10576  pwfseqlem3  10583  hargch  10596  winalim2  10619  gchina  10622  inar1  10698  0npi  10805  mulclpi  10816  mulcanpi  10823  nlt1pi  10829  nqereu  10852  prcdnq  10916  prnmax  10918  ltresr2  11064  axrnegex  11085  axpre-sup  11092  eluz2gt1  12845  1nuz2  12849  zsupss  12862  rpgt0  12930  ixxss1  13291  ixxss2  13292  ixxss12  13293  lbioo  13304  ubioo  13305  iccss2  13345  iccssico2  13348  elfzuz3  13449  serge0  13991  expge0  14033  expge1  14034  expaddzlem  14040  hashrabsn1  14309  hashfun  14372  cshinj  14746  relexpuzrel  14987  shftfn  15008  01sqrexlem6  15182  rlimss  15437  lo1dm  15454  o1dm  15465  rlimrege0  15514  fsumf1o  15658  fsumge0  15730  incexc2  15773  supcvg  15791  fprodf1o  15881  divalglem9  16340  bitsfzolem  16373  bitsf1  16385  gcdcllem1  16438  bezout  16482  nprm  16627  dvdsprm  16642  coprm  16650  dfphi2  16713  phimullem  16718  phisum  16730  expnprm  16842  prmreclem2  16857  prmreclem5  16860  1arith  16867  4sqlem18  16902  vdwnnlem3  16937  ramtlecl  16940  rami  16955  0ram  16960  ramub1lem1  16966  prmgaplem5  16995  acsfiel  17589  isacs1i  17592  catlid  17618  catrid  17619  fullfo  17850  fthf1  17855  fthoppc  17861  invfuc  17913  prslem  18232  oduprs  18235  posi  18252  tleile  18354  resspos  18364  resstos  18365  dlatmjdi  18458  pslem  18507  tsrlin  18520  cnvtsr  18523  tsrdir  18539  mndid  18681  mhmf  18726  mhmlin  18730  mhm0  18731  mndind  18765  grpinvex  18885  grplinv  18931  mulgz  19044  mulgdirlem  19047  mulgdir  19048  mulgass  19053  nsgbi  19098  nmzbi  19105  ghmf  19161  ghmlin  19162  conjnsg  19195  gimf1o  19204  gagrpid  19235  gaf  19236  gaass  19238  psgnunilem5  19435  odid  19479  odf1o2  19514  gexid  19522  sylow1lem4  19542  pj1id  19640  efgredeu  19693  ablcmn  19728  cmncom  19739  mulgdi  19767  torsubg  19795  cyggenod2  19826  cygctb  19833  ghmcyg  19837  dprdf1o  19975  ablfacrplem  20008  ablfaclem2  20029  ablfac2  20032  simpg2nsg  20039  fincygsubgodexd  20056  ogrpinv0le  20077  ogrpsub  20078  ogrpaddlt  20079  crngmgp  20188  rnghmmgmhm  20391  rhmmhm  20427  rhmghm  20431  rimf1o  20440  nzrnz  20460  0ringbas  20473  subrgss  20517  subrg1cl  20525  rnghmsubcsetclem1  20576  zrinitorngc  20587  zrtermorngc  20588  rhmsubcsetclem1  20605  ringcinv  20616  zrtermoringc  20620  rrgeq0i  20644  domneq0  20653  domnrrg  20658  drngunit  20679  fldcrngd  20687  drngmgp  20690  drngid  20691  drngdomn  20694  issubdrg  20725  fldhmsubc  20730  fldsdrgfld  20743  cntzsdrg  20747  abvge0  20762  srngcnv  20792  orngsqr  20811  ornglmulle  20812  orngrmulle  20813  ofldtos  20818  ofldlt1  20820  suborng  20821  subofld  20822  lmhmlin  20999  lmimf1o  21027  lvecdrng  21069  lspsolvlem  21109  islbs3  21122  lbsextlem3  21127  2idlelbas  21231  2idlcpblrng  21238  zringunit  21433  prmirredlem  21439  irinitoringc  21446  znidomb  21528  cygzn  21537  ofldchr  21543  psgndiflemB  21567  pjf  21680  frlmsslsp  21763  frlmlbs  21764  f1lindf  21789  assalem  21824  psrbaglefi  21894  psrbagleadd1  21896  mplelsfi  21962  mplsubrglem  21971  mplcoe1  22004  mplbas2  22009  opsrtoslem2  22023  mhpmulcl  22104  psdmul  22121  coe1mul2  22223  pmatcoe1fsupp  22657  toponuni  22870  tpsuni  22892  mretopd  23048  neips  23069  neiptoptop  23087  neiptopnei  23088  perflp  23110  perfi  23111  cnf  23202  cnpf  23203  cnpimaex  23212  cnima  23221  t0sep  23280  t1ficld  23283  hausnei  23284  pnrmcld  23298  cnrmi  23316  cmpcov  23345  tgcmp  23357  hauscmplem  23362  connclo  23371  1stcclb  23400  2ndcdisj  23412  llyi  23430  nllyi  23431  ptpjpre1  23527  ptpjcn  23567  ptpjopn  23568  ptclsg  23571  dfac14  23574  txdis1cn  23591  pthaus  23594  hauseqlcld  23602  txkgen  23608  xkococn  23616  txconn  23645  hmeocnvcn  23717  fbssfi  23793  filss  23809  uffixfr  23879  flimneiss  23922  flimelbas  23924  flimfnfcls  23984  alexsubb  24002  alexsubALT  24007  ptcmplem2  24009  ptcmplem3  24010  ptcmplem4  24011  tmdgsum2  24052  ghmcnp  24071  tgpt0  24075  qustgplem  24077  istdrg2  24134  vscacn  24142  tvctdrg  24149  uspreg  24229  ucncn  24240  neipcfilu  24251  cuspcvg  24256  psmetxrge0  24269  isxmet2d  24283  prdsxmetlem  24324  imasdsf1olem  24329  xmstopn  24407  mstopn  24408  stdbdxmet  24471  prdsxmslem2  24485  nrgabv  24617  nmvs  24632  nvclvec  24653  nmoge0  24677  nghmcl  24683  nmoi  24684  nghmghm  24690  nmhmlmhm  24705  nmhmnghm  24706  icccmp  24782  xrge0gsumle  24790  metds0  24807  metdstri  24808  metdsre  24810  metdseq0  24811  metdscnlem  24812  metnrmlem1a  24815  icopnfcnv  24908  xrhmeo  24912  pcoval1  24981  cvslvec  25093  cvsunit  25099  recvs  25114  cphreccllem  25146  cphsscph  25219  cmetcvg  25253  lmle  25269  cmscmet  25314  cmetcusp1  25321  hlcph  25332  minveclem4  25400  ivthlem3  25422  ovolmge0  25446  ovolicc1  25485  ovolicc2lem3  25488  ovolicc2lem5  25490  dyadmbl  25569  i1ff  25645  i1frn  25646  i1fima2  25648  itg2monolem1  25719  dvnres  25901  c1liplem1  25969  c1lip2  25971  dvge0  25979  lhop1lem  25986  itgsubstlem  26023  fta1glem2  26142  fta1b  26145  idomrootle  26146  plyf  26171  plypf1  26185  plyadd  26190  plymul  26191  coeeu  26198  dgrlem  26202  coeid  26211  elqaalem3  26297  aareccl  26302  eff1olem  26525  relogf1o  26543  logdmn0  26617  logcnlem2  26620  logcnlem3  26621  efopnlem1  26633  efopnlem2  26634  logtayl2  26639  cxpcn3lem  26725  cxpcn3  26726  logbgcd1irr  26772  atandmneg  26884  atandmcj  26887  efiatan2  26895  cosatan  26899  cosatanne0  26900  dvatan  26913  areage0  26941  cxp2lim  26955  jensenlem2  26966  jensen  26967  eldmgm  27000  dmgmaddn0  27001  dmlogdmgm  27002  lgamgulmlem2  27008  lgamgulmlem3  27009  lgamgulmlem5  27011  lgambdd  27015  lgamucov  27016  ftalem3  27053  efnnfsumcl  27081  efchtdvds  27137  sqff1o  27160  fsumdvdsdiaglem  27161  dvdsppwf1o  27164  dvdsflf1o  27165  musum  27169  muinv  27171  mpodvdsmulf1o  27172  dvdsmulf1o  27174  lgsfle1  27285  lgsle1  27291  lgsdirprm  27310  lgsne0  27314  lgseisenlem3  27356  lgseisenlem4  27357  lgsquadlem1  27359  lgsquadlem2  27360  chebbnd1  27451  chtppilim  27454  chpchtlim  27458  chpo1ub  27459  dchrmusumlema  27472  dchrvmasumlem1  27474  dchrisum0lema  27493  dchrisum0lem2a  27496  logsqvma  27521  selberg3lem2  27537  pntrsumo1  27544  pnt2  27592  ostthlem1  27606  ostth3  27617  ltsval2  27636  leftlt  27861  rightgt  27862  precsexlem8  28222  precsexlem9  28223  precsexlem11  28225  elons2  28266  onleft  28268  ltonold  28269  oncutleft  28271  oncutlt  28272  zcuts0  28416  axtgcgrrflx  28546  axtgcgrid  28547  axtgsegcon  28548  axtg5seg  28549  axtgbtwnid  28550  axtgpasch  28551  axtgcont1  28552  tglng  28630  axcontlem7  29055  axcontlem10  29058  upgrle  29175  umgredg2  29185  lfgredgge2  29209  usgredg2ALT  29278  usgr1vr  29340  usgrexmpledg  29347  upgrres1  29398  fusgrvtxfi  29404  vtxnbuvtx  29476  cusgrcplgr  29505  vdumgr0  29566  vtxdgoddnumeven  29639  trlres  29784  usgr2pth  29849  cyclispthon  29889  clwwlknlen  30119  clwwnonrepclwwnon  30432  2clwwlk2  30435  ablocom  30635  phpar2  30910  cbncms  30952  hlph  30976  hcaucvg  31273  hlimconvi  31278  shaddcl  31304  shmulcl  31305  chlimi  31321  chcompl  31329  choc1  31414  nmopre  31957  cnopc  32000  lnopl  32001  unop  32002  hmop  32009  cnfnc  32017  lnfnl  32018  nlelshi  32147  cnlnadjlem5  32158  elpjidm  32271  mdslle1i  32404  mdslle2i  32405  atcv0  32429  aciunf1lem  32751  padct  32807  ssnnssfz  32877  ccatf1  33041  swrdrndisj  33049  ressprs  33058  pwrssmgc  33092  wrdpmtrlast  33186  cyc3evpm  33243  cycpmgcl  33246  cycpmconjslem2  33248  cyc3conja  33250  isarchi3  33280  archirng  33281  archirngz  33282  archiabllem1a  33284  archiabllem1b  33285  archiabllem2a  33287  archiabllem2c  33288  archiabllem2b  33289  archiabl  33291  isarchiofld  33292  elrgspnlem1  33335  elrgspnlem2  33336  elrgspnlem4  33338  elrgspnsubrun  33342  isdrng4  33388  nn0omnd  33436  quslsm  33497  nsgmgclem  33503  nsgmgc  33504  prmidl0  33542  qsidomlem1  33544  mxidlirred  33564  krull  33571  ufdprmidl  33633  1arithufdlem4  33639  extvfvcl  33712  mplvrpmlem  33719  mplvrpmga  33721  sradrng  33758  extdg1id  33843  ply1annnr  33880  madjusmdetlem4  34007  qtophaus  34013  crefi  34024  cmpcref  34027  cmppcmp  34035  pcmplfin  34037  zart0  34056  tpr2rico  34089  rge0scvg  34126  zrhunitpreima  34153  qqhrhm  34166  esummono  34231  gsumesum  34236  esumrnmpt2  34245  esumpinfval  34250  esumpcvgval  34255  esumpmono  34256  0elsiga  34291  sigaclcu  34294  issgon  34300  inelpisys  34331  ldsysgenld  34337  ldgenpisyslem1  34340  sxuni  34370  isrnmeas  34377  measvuni  34391  measssd  34392  ddemeas  34413  imambfm  34439  elmbfmvol2  34444  dya2icoseg2  34455  omssubaddlem  34476  omssubadd  34477  carsgsigalem  34492  pmeasmono  34501  sibfinima  34516  oddpwdc  34531  oddpwdcv  34532  eulerpartlemf  34547  eulerpartlemt  34548  eulerpartlemr  34551  eulerpartlemgvv  34553  eulerpartlemgs2  34557  fiblem  34575  probtot  34589  ballotlem4  34676  ballotlem5  34677  ballotlemfrc  34704  ballotlemirc  34709  ballotth  34715  hgt750lemb  34833  bnj642  34924  bnj643  34925  bnj645  34926  bnj707  34931  bnj1379  35005  bnj1538  35030  bnj110  35033  bnj93  35038  bnj906  35105  bnj1006  35135  bnj1110  35157  bnj1121  35160  bnj1204  35187  bnj1321  35202  bnj1364  35203  bnj1398  35209  bnj1450  35225  bnj1312  35233  bnj1501  35242  bnj1523  35246  tz9.1regs  35309  0nn0m1nnn0  35326  subfacp1lem3  35395  subfacp1lem5  35397  pconncn  35437  connpconn  35448  cvmcov  35476  cvmliftlem1  35498  cvmliftlem10  35507  cvmlift2lem11  35526  cvmlift2lem12  35527  msubff1  35769  mvhf1  35772  mthmpps  35795  mclspps  35797  fundmpss  35980  funpartfun  36156  fnetg  36558  neibastop1  36572  filnetlem3  36593  onint1  36662  weiunlem  36676  weiunpo  36678  weiunse  36681  bj-nnfa  36967  bj-idres  37404  bj-rvecrr  37541  icorempo  37595  pibt2  37661  wl-nfeqfb  37780  phpreu  37844  fin2solem  37846  fin2so  37847  lindsenlbs  37855  matunitlindflem1  37856  matunitlindflem2  37857  matunitlindf  37858  ptrest  37859  poimirlem1  37861  poimirlem2  37862  poimirlem3  37863  poimirlem4  37864  poimirlem5  37865  poimirlem6  37866  poimirlem7  37867  poimirlem8  37868  poimirlem9  37869  poimirlem10  37870  poimirlem11  37871  poimirlem12  37872  poimirlem13  37873  poimirlem14  37874  poimirlem15  37875  poimirlem16  37876  poimirlem17  37877  poimirlem18  37878  poimirlem19  37879  poimirlem20  37880  poimirlem21  37881  poimirlem22  37882  poimirlem23  37883  poimirlem24  37884  poimirlem26  37886  poimirlem27  37887  poimirlem29  37889  poimirlem31  37891  mblfinlem2  37898  dvtan  37910  itg2gt0cn  37915  ftc1anclem7  37939  ftc1anclem8  37940  ftc1anc  37941  cover2  37955  indexa  37973  istotbnd3  38011  sstotbnd2  38014  sstotbnd  38015  totbndss  38017  equivtotbnd  38018  isbnd3  38024  totbndbnd  38029  equivbnd  38030  prdsbnd  38033  prdstotbnd  38034  heibor  38061  zrdivrng  38193  crngocom  38241  isfld2  38245  dmncrng  38296  eqvrelrel  38921  disjrel  39070  disjdmqscossss  39146  prter2  39246  toycom  39338  lsateln0  39360  lpssat  39378  lssat  39381  oposlem  39547  olop  39579  omllaw  39608  cvlexch1  39693  dihpN  41701  mapdordlem2  42002  linvh  42455  idomnnzpownz  42491  idomnnzgmulnz  42492  aks6d1c5lem2  42497  deg1pow  42500  redvmptabs  42719  readvrec2  42720  readvrec  42721  mhphflem  42943  prjspertr  42952  nacsfg  43051  nacsfix  43058  mzpindd  43092  diophrw  43105  diophrex  43121  rexzrexnn0  43150  pell1234qrdich  43207  rmspecnonsq  43253  rmspecfund  43255  rmspecpos  43262  monotoddzzfi  43288  ltrmxnn0  43295  rmxnn  43297  jm2.23  43342  jm3.1lem2  43364  dnnumch3  43393  lnmlssfg  43426  lnmlmic  43434  lnrlnm  43459  lnr2i  43462  lpirlnr  43463  hbtlem6  43475  hbt  43476  mnccoe  43484  proot1mul  43540  proot1hash  43541  deg1mhm  43546  ondif1i  43608  limnsuc  43611  cantnfresb  43670  succlg  43674  ntrneifv2  44425  grucollcld  44605  mnurndlem1  44626  ismnushort  44646  radcnvrat  44659  binomcxplemdvbinom  44698  binomcxplemcvg  44699  binomcxplemnotnn0  44701  ordelordALT  44882  2uasbanh  44906  ordelordALTVD  45211  relprel  45296  elixpconstg  45437  rabidim2  45450  disjinfi  45540  supminfxr2  45816  sumnnodd  45979  stoweidlem7  46354  stoweidlem14  46361  stoweidlem16  46363  stoweidlem24  46371  stoweidlem31  46378  stoweidlem54  46401  wallispilem3  46414  fourierdlem42  46496  fourierdlem48  46501  fourierdlem51  46504  fourierdlem64  46517  fourierdlem76  46529  fourierdlem79  46532  fourierdlem81  46534  fourierdlem87  46540  etransclem28  46609  etransclem32  46613  sge0fodjrnlem  46763  hoidmvlelem3  46944  ovolval5lem3  47001  pimrecltpos  47055  pimrecltneg  47071  issmflem  47074  smfaddlem1  47110  smfsuplem1  47158  smfsuplem3  47160  smflimsuplem7  47173  smfliminflem  47177  nfunsnafv  47491  faovcl  47549  tz6.12-2-afv2  47586  tz6.12i-afv2  47592  sprel  47833  evendiv2z  47981  oddp1div2z  47982  2dvdseven  48002  2ndvdsodd  48004  perfectALTVlem1  48070  sbgoldbm  48133  upgrimtrls  48255  upgrimpthslem1  48256  upgrimspths  48259  upgrimcycls  48260  uhgrimisgrgric  48280  gpgprismgr4cycllem2  48445  clintopcllaw  48560  uzlidlring  48584  rngccatidALTV  48621  funcringcsetcALTV2lem7  48645  ringccatidALTV  48655  ringcinvALTV  48659  funcringcsetclem7ALTV  48668  fldhmsubcALTV  48682  ssnn0ssfz  48698  el0ldepsnzr  48816  regt1loggt0  48885  elbigodm  48904  fllogbd  48909  rrx2xpref1o  49067  unilbss  49166  fdomne0  49198  f002  49202  xpco2  49205  imaf1homlem  49455  idemb  49507  uobeq2  49749  thincmo2  49774  thincmoALT  49777  fullthinc  49798  idfudiag1  49873  elsetrecslem  50047