Theorem simprbi 496

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  1520  eumo  2578  reurmo  3353  pssne  4051  pssn2lp  4056  ssnpss  4058  eldifn  4084  elinel2  4154  rabsnt  4688  eldifsni  4746  unimax  4900  ssintub  4921  moop2  5450  pwssun  5516  weso  5615  opelxp2  5667  predpo  6281  frpoinsg  6301  ordwe  6330  funmo  6508  funopg  6526  funun  6538  fununi  6567  funimaexg  6579  fndm  6595  frn  6669  f1ss  6735  f1ssr  6736  forn  6749  f1f1orn  6785  f1orescnv  6789  f1imacnv  6790  funcocnv2  6799  dffv2  6929  exfo  7050  foelrn  7052  foelrnf  7053  isorel  7272  isoini2  7285  f1ofveu  7352  fovcld  7485  onminesb  7738  onminsb  7739  tfisg  7796  tfis  7797  limomss  7813  nnlim  7822  ssnlim  7828  resf1ext2b  7877  curry1  8046  curry2  8049  f1o2ndf1  8064  fnwelem  8073  mpoxopn0yelv  8155  tz7.48lem  8372  dif20el  8432  oeordi  8515  oeeulem  8529  oeeui  8530  nnawordex  8565  swoer  8666  eceqoveq  8759  mapsnconst  8830  resixpfo  8874  boxcutc  8879  sdomnen  8918  en0  8955  en0ALT  8956  en0r  8957  en1  8961  dom0  9033  fodomr  9056  dif1enlem  9084  unxpdomlem3  9158  fineqvlem  9166  infn0  9202  fodomfir  9228  f1opwfi  9256  fsuppcolem  9304  fsuppco  9305  mapfienlem1  9308  mapfienlem2  9309  supub  9362  suplub  9363  ordtypelem2  9424  ordtypelem3  9425  ordtypelem6  9428  ordtypelem7  9429  wemapso2lem  9457  wdom2d  9485  brwdom3  9487  ixpiunwdom  9495  inf3lem2  9538  inf3lem6  9542  oancom  9560  infdifsn  9566  cantnfp1lem3  9589  cantnflem3  9600  cantnflem4  9601  oef1o  9607  cnfcom3  9613  tctr  9647  frinsg  9663  tz9.12lem3  9701  scottex  9797  cardid2  9865  infxpenlem  9923  acni3  9957  cardaleph  9999  iscard3  10003  dfac5lem4  10036  dfac5lem5  10037  dfac5lem4OLD  10038  kmlem1  10061  cofsmo  10179  fin4en1  10219  enfin2i  10231  fin23lem28  10250  fin23lem38  10259  isf32lem6  10268  enfin1ai  10294  hsmexlem2  10337  hsmexlem4  10339  domtriomlem  10352  axdc2lem  10358  axdc3lem2  10361  ac6num  10389  zorn2lem2  10407  brdom3  10438  alephval2  10483  alephreg  10493  pwcfsdom  10494  smobeth  10497  fpwwe2lem5  10546  fpwwe2lem12  10553  canthp1lem2  10564  pwfseqlem3  10571  hargch  10584  winalim2  10607  gchina  10610  inar1  10686  0npi  10793  mulclpi  10804  mulcanpi  10811  nlt1pi  10817  nqereu  10840  prcdnq  10904  prnmax  10906  ltresr2  11052  axrnegex  11073  axpre-sup  11080  eluz2gt1  12833  1nuz2  12837  zsupss  12850  rpgt0  12918  ixxss1  13279  ixxss2  13280  ixxss12  13281  lbioo  13292  ubioo  13293  iccss2  13333  iccssico2  13336  elfzuz3  13437  serge0  13979  expge0  14021  expge1  14022  expaddzlem  14028  hashrabsn1  14297  hashfun  14360  cshinj  14734  relexpuzrel  14975  shftfn  14996  01sqrexlem6  15170  rlimss  15425  lo1dm  15442  o1dm  15453  rlimrege0  15502  fsumf1o  15646  fsumge0  15718  incexc2  15761  supcvg  15779  fprodf1o  15869  divalglem9  16328  bitsfzolem  16361  bitsf1  16373  gcdcllem1  16426  bezout  16470  nprm  16615  dvdsprm  16630  coprm  16638  dfphi2  16701  phimullem  16706  phisum  16718  expnprm  16830  prmreclem2  16845  prmreclem5  16848  1arith  16855  4sqlem18  16890  vdwnnlem3  16925  ramtlecl  16928  rami  16943  0ram  16948  ramub1lem1  16954  prmgaplem5  16983  acsfiel  17577  isacs1i  17580  catlid  17606  catrid  17607  fullfo  17838  fthf1  17843  fthoppc  17849  invfuc  17901  prslem  18220  oduprs  18223  posi  18240  tleile  18342  resspos  18352  resstos  18353  dlatmjdi  18446  pslem  18495  tsrlin  18508  cnvtsr  18511  tsrdir  18527  mndid  18669  mhmf  18714  mhmlin  18718  mhm0  18719  mndind  18753  grpinvex  18873  grplinv  18919  mulgz  19032  mulgdirlem  19035  mulgdir  19036  mulgass  19041  nsgbi  19086  nmzbi  19093  ghmf  19149  ghmlin  19150  conjnsg  19183  gimf1o  19192  gagrpid  19223  gaf  19224  gaass  19226  psgnunilem5  19423  odid  19467  odf1o2  19502  gexid  19510  sylow1lem4  19530  pj1id  19628  efgredeu  19681  ablcmn  19716  cmncom  19727  mulgdi  19755  torsubg  19783  cyggenod2  19814  cygctb  19821  ghmcyg  19825  dprdf1o  19963  ablfacrplem  19996  ablfaclem2  20017  ablfac2  20020  simpg2nsg  20027  fincygsubgodexd  20044  ogrpinv0le  20065  ogrpsub  20066  ogrpaddlt  20067  crngmgp  20176  rnghmmgmhm  20379  rhmmhm  20415  rhmghm  20419  rimf1o  20428  nzrnz  20448  0ringbas  20461  subrgss  20505  subrg1cl  20513  rnghmsubcsetclem1  20564  zrinitorngc  20575  zrtermorngc  20576  rhmsubcsetclem1  20593  ringcinv  20604  zrtermoringc  20608  rrgeq0i  20632  domneq0  20641  domnrrg  20646  drngunit  20667  fldcrngd  20675  drngmgp  20678  drngid  20679  drngdomn  20682  issubdrg  20713  fldhmsubc  20718  fldsdrgfld  20731  cntzsdrg  20735  abvge0  20750  srngcnv  20780  orngsqr  20799  ornglmulle  20800  orngrmulle  20801  ofldtos  20806  ofldlt1  20808  suborng  20809  subofld  20810  lmhmlin  20987  lmimf1o  21015  lvecdrng  21057  lspsolvlem  21097  islbs3  21110  lbsextlem3  21115  2idlelbas  21219  2idlcpblrng  21226  zringunit  21421  prmirredlem  21427  irinitoringc  21434  znidomb  21516  cygzn  21525  ofldchr  21531  psgndiflemB  21555  pjf  21668  frlmsslsp  21751  frlmlbs  21752  f1lindf  21777  assalem  21812  psrbaglefi  21882  psrbagleadd1  21884  mplelsfi  21950  mplsubrglem  21959  mplcoe1  21992  mplbas2  21997  opsrtoslem2  22011  mhpmulcl  22092  psdmul  22109  coe1mul2  22211  pmatcoe1fsupp  22645  toponuni  22858  tpsuni  22880  mretopd  23036  neips  23057  neiptoptop  23075  neiptopnei  23076  perflp  23098  perfi  23099  cnf  23190  cnpf  23191  cnpimaex  23200  cnima  23209  t0sep  23268  t1ficld  23271  hausnei  23272  pnrmcld  23286  cnrmi  23304  cmpcov  23333  tgcmp  23345  hauscmplem  23350  connclo  23359  1stcclb  23388  2ndcdisj  23400  llyi  23418  nllyi  23419  ptpjpre1  23515  ptpjcn  23555  ptpjopn  23556  ptclsg  23559  dfac14  23562  txdis1cn  23579  pthaus  23582  hauseqlcld  23590  txkgen  23596  xkococn  23604  txconn  23633  hmeocnvcn  23705  fbssfi  23781  filss  23797  uffixfr  23867  flimneiss  23910  flimelbas  23912  flimfnfcls  23972  alexsubb  23990  alexsubALT  23995  ptcmplem2  23997  ptcmplem3  23998  ptcmplem4  23999  tmdgsum2  24040  ghmcnp  24059  tgpt0  24063  qustgplem  24065  istdrg2  24122  vscacn  24130  tvctdrg  24137  uspreg  24217  ucncn  24228  neipcfilu  24239  cuspcvg  24244  psmetxrge0  24257  isxmet2d  24271  prdsxmetlem  24312  imasdsf1olem  24317  xmstopn  24395  mstopn  24396  stdbdxmet  24459  prdsxmslem2  24473  nrgabv  24605  nmvs  24620  nvclvec  24641  nmoge0  24665  nghmcl  24671  nmoi  24672  nghmghm  24678  nmhmlmhm  24693  nmhmnghm  24694  icccmp  24770  xrge0gsumle  24778  metds0  24795  metdstri  24796  metdsre  24798  metdseq0  24799  metdscnlem  24800  metnrmlem1a  24803  icopnfcnv  24896  xrhmeo  24900  pcoval1  24969  cvslvec  25081  cvsunit  25087  recvs  25102  cphreccllem  25134  cphsscph  25207  cmetcvg  25241  lmle  25257  cmscmet  25302  cmetcusp1  25309  hlcph  25320  minveclem4  25388  ivthlem3  25410  ovolmge0  25434  ovolicc1  25473  ovolicc2lem3  25476  ovolicc2lem5  25478  dyadmbl  25557  i1ff  25633  i1frn  25634  i1fima2  25636  itg2monolem1  25707  dvnres  25889  c1liplem1  25957  c1lip2  25959  dvge0  25967  lhop1lem  25974  itgsubstlem  26011  fta1glem2  26130  fta1b  26133  idomrootle  26134  plyf  26159  plypf1  26173  plyadd  26178  plymul  26179  coeeu  26186  dgrlem  26190  coeid  26199  elqaalem3  26285  aareccl  26290  eff1olem  26513  relogf1o  26531  logdmn0  26605  logcnlem2  26608  logcnlem3  26609  efopnlem1  26621  efopnlem2  26622  logtayl2  26627  cxpcn3lem  26713  cxpcn3  26714  logbgcd1irr  26760  atandmneg  26872  atandmcj  26875  efiatan2  26883  cosatan  26887  cosatanne0  26888  dvatan  26901  areage0  26929  cxp2lim  26943  jensenlem2  26954  jensen  26955  eldmgm  26988  dmgmaddn0  26989  dmlogdmgm  26990  lgamgulmlem2  26996  lgamgulmlem3  26997  lgamgulmlem5  26999  lgambdd  27003  lgamucov  27004  ftalem3  27041  efnnfsumcl  27069  efchtdvds  27125  sqff1o  27148  fsumdvdsdiaglem  27149  dvdsppwf1o  27152  dvdsflf1o  27153  musum  27157  muinv  27159  mpodvdsmulf1o  27160  dvdsmulf1o  27162  lgsfle1  27273  lgsle1  27279  lgsdirprm  27298  lgsne0  27302  lgseisenlem3  27344  lgseisenlem4  27345  lgsquadlem1  27347  lgsquadlem2  27348  chebbnd1  27439  chtppilim  27442  chpchtlim  27446  chpo1ub  27447  dchrmusumlema  27460  dchrvmasumlem1  27462  dchrisum0lema  27481  dchrisum0lem2a  27484  logsqvma  27509  selberg3lem2  27525  pntrsumo1  27532  pnt2  27580  ostthlem1  27594  ostth3  27605  ltsval2  27624  leftlt  27849  rightgt  27850  precsexlem8  28210  precsexlem9  28211  precsexlem11  28213  elons2  28254  onleft  28256  ltonold  28257  oncutleft  28259  oncutlt  28260  zcuts0  28404  axtgcgrrflx  28534  axtgcgrid  28535  axtgsegcon  28536  axtg5seg  28537  axtgbtwnid  28538  axtgpasch  28539  axtgcont1  28540  tglng  28618  axcontlem7  29043  axcontlem10  29046  upgrle  29163  umgredg2  29173  lfgredgge2  29197  usgredg2ALT  29266  usgr1vr  29328  usgrexmpledg  29335  upgrres1  29386  fusgrvtxfi  29392  vtxnbuvtx  29464  cusgrcplgr  29493  vdumgr0  29554  vtxdgoddnumeven  29627  trlres  29772  usgr2pth  29837  cyclispthon  29877  clwwlknlen  30107  clwwnonrepclwwnon  30420  2clwwlk2  30423  ablocom  30623  phpar2  30898  cbncms  30940  hlph  30964  hcaucvg  31261  hlimconvi  31266  shaddcl  31292  shmulcl  31293  chlimi  31309  chcompl  31317  choc1  31402  nmopre  31945  cnopc  31988  lnopl  31989  unop  31990  hmop  31997  cnfnc  32005  lnfnl  32006  nlelshi  32135  cnlnadjlem5  32146  elpjidm  32259  mdslle1i  32392  mdslle2i  32393  atcv0  32417  aciunf1lem  32740  padct  32797  ssnnssfz  32867  ccatf1  33031  swrdrndisj  33039  ressprs  33048  pwrssmgc  33082  wrdpmtrlast  33175  cyc3evpm  33232  cycpmgcl  33235  cycpmconjslem2  33237  cyc3conja  33239  isarchi3  33269  archirng  33270  archirngz  33271  archiabllem1a  33273  archiabllem1b  33274  archiabllem2a  33276  archiabllem2c  33277  archiabllem2b  33278  archiabl  33280  isarchiofld  33281  elrgspnlem1  33324  elrgspnlem2  33325  elrgspnlem4  33327  elrgspnsubrun  33331  isdrng4  33377  nn0omnd  33425  quslsm  33486  nsgmgclem  33492  nsgmgc  33493  prmidl0  33531  qsidomlem1  33533  mxidlirred  33553  krull  33560  ufdprmidl  33622  1arithufdlem4  33628  extvfvcl  33701  mplvrpmlem  33708  mplvrpmga  33710  sradrng  33738  extdg1id  33823  ply1annnr  33860  madjusmdetlem4  33987  qtophaus  33993  crefi  34004  cmpcref  34007  cmppcmp  34015  pcmplfin  34017  zart0  34036  tpr2rico  34069  rge0scvg  34106  zrhunitpreima  34133  qqhrhm  34146  esummono  34211  gsumesum  34216  esumrnmpt2  34225  esumpinfval  34230  esumpcvgval  34235  esumpmono  34236  0elsiga  34271  sigaclcu  34274  issgon  34280  inelpisys  34311  ldsysgenld  34317  ldgenpisyslem1  34320  sxuni  34350  isrnmeas  34357  measvuni  34371  measssd  34372  ddemeas  34393  imambfm  34419  elmbfmvol2  34424  dya2icoseg2  34435  omssubaddlem  34456  omssubadd  34457  carsgsigalem  34472  pmeasmono  34481  sibfinima  34496  oddpwdc  34511  oddpwdcv  34512  eulerpartlemf  34527  eulerpartlemt  34528  eulerpartlemr  34531  eulerpartlemgvv  34533  eulerpartlemgs2  34537  fiblem  34555  probtot  34569  ballotlem4  34656  ballotlem5  34657  ballotlemfrc  34684  ballotlemirc  34689  ballotth  34695  hgt750lemb  34813  bnj642  34904  bnj643  34905  bnj645  34906  bnj707  34911  bnj1379  34986  bnj1538  35011  bnj110  35014  bnj93  35019  bnj906  35086  bnj1006  35116  bnj1110  35138  bnj1121  35141  bnj1204  35168  bnj1321  35183  bnj1364  35184  bnj1398  35190  bnj1450  35206  bnj1312  35214  bnj1501  35223  bnj1523  35227  tz9.1regs  35290  0nn0m1nnn0  35307  subfacp1lem3  35376  subfacp1lem5  35378  pconncn  35418  connpconn  35429  cvmcov  35457  cvmliftlem1  35479  cvmliftlem10  35488  cvmlift2lem11  35507  cvmlift2lem12  35508  msubff1  35750  mvhf1  35753  mthmpps  35776  mclspps  35778  fundmpss  35961  funpartfun  36137  fnetg  36539  neibastop1  36553  filnetlem3  36574  onint1  36643  weiunlem  36657  weiunpo  36659  weiunse  36662  bj-nnfa  36929  bj-idres  37365  bj-rvecrr  37502  icorempo  37556  pibt2  37622  wl-nfeqfb  37741  phpreu  37805  fin2solem  37807  fin2so  37808  lindsenlbs  37816  matunitlindflem1  37817  matunitlindflem2  37818  matunitlindf  37819  ptrest  37820  poimirlem1  37822  poimirlem2  37823  poimirlem3  37824  poimirlem4  37825  poimirlem5  37826  poimirlem6  37827  poimirlem7  37828  poimirlem8  37829  poimirlem9  37830  poimirlem10  37831  poimirlem11  37832  poimirlem12  37833  poimirlem13  37834  poimirlem14  37835  poimirlem15  37836  poimirlem16  37837  poimirlem17  37838  poimirlem18  37839  poimirlem19  37840  poimirlem20  37841  poimirlem21  37842  poimirlem22  37843  poimirlem23  37844  poimirlem24  37845  poimirlem26  37847  poimirlem27  37848  poimirlem29  37850  poimirlem31  37852  mblfinlem2  37859  dvtan  37871  itg2gt0cn  37876  ftc1anclem7  37900  ftc1anclem8  37901  ftc1anc  37902  cover2  37916  indexa  37934  istotbnd3  37972  sstotbnd2  37975  sstotbnd  37976  totbndss  37978  equivtotbnd  37979  isbnd3  37985  totbndbnd  37990  equivbnd  37991  prdsbnd  37994  prdstotbnd  37995  heibor  38022  zrdivrng  38154  crngocom  38202  isfld2  38206  dmncrng  38257  eqvrelrel  38854  disjrel  38989  disjdmqscossss  39062  prter2  39141  toycom  39233  lsateln0  39255  lpssat  39273  lssat  39276  oposlem  39442  olop  39474  omllaw  39503  cvlexch1  39588  dihpN  41596  mapdordlem2  41897  linvh  42350  idomnnzpownz  42386  idomnnzgmulnz  42387  aks6d1c5lem2  42392  deg1pow  42395  redvmptabs  42615  readvrec2  42616  readvrec  42617  mhphflem  42839  prjspertr  42848  nacsfg  42947  nacsfix  42954  mzpindd  42988  diophrw  43001  diophrex  43017  rexzrexnn0  43046  pell1234qrdich  43103  rmspecnonsq  43149  rmspecfund  43151  rmspecpos  43158  monotoddzzfi  43184  ltrmxnn0  43191  rmxnn  43193  jm2.23  43238  jm3.1lem2  43260  dnnumch3  43289  lnmlssfg  43322  lnmlmic  43330  lnrlnm  43355  lnr2i  43358  lpirlnr  43359  hbtlem6  43371  hbt  43372  mnccoe  43380  proot1mul  43436  proot1hash  43437  deg1mhm  43442  ondif1i  43504  limnsuc  43507  cantnfresb  43566  succlg  43570  ntrneifv2  44321  grucollcld  44501  mnurndlem1  44522  ismnushort  44542  radcnvrat  44555  binomcxplemdvbinom  44594  binomcxplemcvg  44595  binomcxplemnotnn0  44597  ordelordALT  44778  2uasbanh  44802  ordelordALTVD  45107  relprel  45192  elixpconstg  45333  rabidim2  45346  disjinfi  45436  supminfxr2  45713  sumnnodd  45876  stoweidlem7  46251  stoweidlem14  46258  stoweidlem16  46260  stoweidlem24  46268  stoweidlem31  46275  stoweidlem54  46298  wallispilem3  46311  fourierdlem42  46393  fourierdlem48  46398  fourierdlem51  46401  fourierdlem64  46414  fourierdlem76  46426  fourierdlem79  46429  fourierdlem81  46431  fourierdlem87  46437  etransclem28  46506  etransclem32  46510  sge0fodjrnlem  46660  hoidmvlelem3  46841  ovolval5lem3  46898  pimrecltpos  46952  pimrecltneg  46968  issmflem  46971  smfaddlem1  47007  smfsuplem1  47055  smfsuplem3  47057  smflimsuplem7  47070  smfliminflem  47074  nfunsnafv  47388  faovcl  47446  tz6.12-2-afv2  47483  tz6.12i-afv2  47489  sprel  47730  evendiv2z  47878  oddp1div2z  47879  2dvdseven  47899  2ndvdsodd  47901  perfectALTVlem1  47967  sbgoldbm  48030  upgrimtrls  48152  upgrimpthslem1  48153  upgrimspths  48156  upgrimcycls  48157  uhgrimisgrgric  48177  gpgprismgr4cycllem2  48342  clintopcllaw  48457  uzlidlring  48481  rngccatidALTV  48518  funcringcsetcALTV2lem7  48542  ringccatidALTV  48552  ringcinvALTV  48556  funcringcsetclem7ALTV  48565  fldhmsubcALTV  48579  ssnn0ssfz  48595  el0ldepsnzr  48713  regt1loggt0  48782  elbigodm  48801  fllogbd  48806  rrx2xpref1o  48964  unilbss  49063  fdomne0  49095  f002  49099  xpco2  49102  imaf1homlem  49352  idemb  49404  uobeq2  49646  thincmo2  49671  thincmoALT  49674  fullthinc  49695  idfudiag1  49770  elsetrecslem  49944