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  1515  eumo  2575  reurmo  3380  pssne  4108  pssn2lp  4113  ssnpss  4115  eldifn  4141  elinel2  4211  rabsnt  4735  eldifsni  4794  unimax  4948  ssintub  4970  moop2  5511  pwssun  5579  weso  5679  opelxp2  5731  predpo  6345  frpoinsg  6365  wfisgOLD  6376  ordwe  6398  funmo  6582  funmoOLD  6583  funopg  6601  funun  6613  fununi  6642  funimaexg  6653  fndm  6671  frn  6743  f1ss  6809  f1ssr  6810  forn  6823  f1f1orn  6859  f1orescnv  6863  f1imacnv  6864  funcocnv2  6873  dffv2  7003  exfo  7124  foelrn  7126  foelrnf  7127  isorel  7345  isoini2  7358  f1ofveu  7424  fovcld  7559  onminesb  7812  onminsb  7813  tfisg  7874  tfis  7875  limomss  7891  nnlim  7900  ssnlim  7906  curry1  8127  curry2  8130  f1o2ndf1  8145  fnwelem  8154  mpoxopn0yelv  8236  wfrlem5OLD  8351  tz7.48lem  8479  dif20el  8541  oeordi  8623  oeeulem  8637  oeeui  8638  nnawordex  8673  swoer  8774  eceqoveq  8860  mapsnconst  8930  resixpfo  8974  boxcutc  8979  sdomnen  9019  en0  9056  en0ALT  9057  en0r  9058  en1  9062  dom0  9140  fodomr  9166  dif1enlem  9194  dif1enlemOLD  9195  unxpdomlem3  9285  fineqvlem  9295  infn0  9337  fodomfir  9365  f1opwfi  9393  fsuppcolem  9438  fsuppco  9439  mapfienlem1  9442  mapfienlem2  9443  supub  9496  suplub  9497  ordtypelem2  9556  ordtypelem3  9557  ordtypelem6  9560  ordtypelem7  9561  wemapso2lem  9589  wdom2d  9617  brwdom3  9619  ixpiunwdom  9627  inf3lem2  9666  inf3lem6  9670  oancom  9688  infdifsn  9694  cantnfp1lem3  9717  cantnflem3  9728  cantnflem4  9729  oef1o  9735  cnfcom3  9741  tctr  9777  frinsg  9788  tz9.12lem3  9826  scottex  9922  cardid2  9990  infxpenlem  10050  acni3  10084  cardaleph  10126  iscard3  10130  dfac5lem4  10163  dfac5lem5  10164  dfac5lem4OLD  10165  kmlem1  10188  cofsmo  10306  fin4en1  10346  enfin2i  10358  fin23lem28  10377  fin23lem38  10386  isf32lem6  10395  enfin1ai  10421  hsmexlem2  10464  hsmexlem4  10466  domtriomlem  10479  axdc2lem  10485  axdc3lem2  10488  ac6num  10516  zorn2lem2  10534  brdom3  10565  alephval2  10609  alephreg  10619  pwcfsdom  10620  smobeth  10623  fpwwe2lem5  10672  fpwwe2lem12  10679  canthp1lem2  10690  pwfseqlem3  10697  hargch  10710  winalim2  10733  gchina  10736  inar1  10812  0npi  10919  mulclpi  10930  mulcanpi  10937  nlt1pi  10943  nqereu  10966  prcdnq  11030  prnmax  11032  ltresr2  11178  axrnegex  11199  axpre-sup  11206  eluz2gt1  12959  1nuz2  12963  zsupss  12976  rpgt0  13044  ixxss1  13401  ixxss2  13402  ixxss12  13403  lbioo  13414  ubioo  13415  iccss2  13454  iccssico2  13457  elfzuz3  13557  serge0  14093  expge0  14135  expge1  14136  expaddzlem  14142  hashrabsn1  14409  hashfun  14472  cshinj  14845  relexpuzrel  15087  shftfn  15108  01sqrexlem6  15282  rlimss  15534  lo1dm  15551  o1dm  15562  rlimrege0  15611  fsumf1o  15755  fsumge0  15827  incexc2  15870  supcvg  15888  fprodf1o  15978  divalglem9  16434  bitsfzolem  16467  bitsf1  16479  gcdcllem1  16532  bezout  16576  nprm  16721  dvdsprm  16736  coprm  16744  dfphi2  16807  phimullem  16812  phisum  16823  expnprm  16935  prmreclem2  16950  prmreclem5  16953  1arith  16960  4sqlem18  16995  vdwnnlem3  17030  ramtlecl  17033  rami  17048  0ram  17053  ramub1lem1  17059  prmgaplem5  17088  acsfiel  17698  isacs1i  17701  catlid  17727  catrid  17728  fullfo  17965  fthf1  17970  fthoppc  17976  invfuc  18030  prslem  18354  oduprs  18357  posi  18374  tleile  18478  dlatmjdi  18580  pslem  18629  tsrlin  18642  cnvtsr  18645  tsrdir  18661  mndid  18769  mhmf  18814  mhmlin  18818  mhm0  18819  mndind  18853  grpinvex  18973  grplinv  19019  mulgz  19132  mulgdirlem  19135  mulgdir  19136  mulgass  19141  nsgbi  19187  nmzbi  19194  ghmf  19250  ghmlin  19251  conjnsg  19284  gimf1o  19293  gagrpid  19324  gaf  19325  gaass  19327  psgnunilem5  19526  odid  19570  odf1o2  19605  gexid  19613  sylow1lem4  19633  pj1id  19731  efgredeu  19784  ablcmn  19819  cmncom  19830  mulgdi  19858  torsubg  19886  cyggenod2  19917  cygctb  19924  ghmcyg  19928  dprdf1o  20066  ablfacrplem  20099  ablfaclem2  20120  ablfac2  20123  simpg2nsg  20130  fincygsubgodexd  20147  crngmgp  20258  rnghmmgmhm  20459  rhmmhm  20495  rhmghm  20500  rimf1o  20510  nzrnz  20531  0ringbas  20544  subrgss  20588  subrg1cl  20596  rnghmsubcsetclem1  20647  zrinitorngc  20658  zrtermorngc  20659  rhmsubcsetclem1  20676  ringcinv  20687  zrtermoringc  20691  rrgeq0i  20715  domneq0  20724  domnrrg  20729  drngunit  20750  fldcrngd  20758  drngmgp  20761  drngid  20762  drngdomn  20765  fldidomOLD  20788  issubdrg  20797  fldhmsubc  20802  fldsdrgfld  20815  cntzsdrg  20819  abvge0  20834  srngcnv  20864  lmhmlin  21051  lmimf1o  21079  lvecdrng  21121  lspsolvlem  21161  islbs3  21174  lbsextlem3  21179  2idlelbas  21291  2idlcpblrng  21298  zringunit  21494  prmirredlem  21500  irinitoringc  21507  znidomb  21597  cygzn  21606  psgndiflemB  21635  pjf  21750  frlmsslsp  21833  frlmlbs  21834  f1lindf  21859  assalem  21894  psrbaglefi  21963  psrbagleadd1  21965  mplelsfi  22032  mplsubrglem  22041  mplcoe1  22072  mplbas2  22077  opsrtoslem2  22097  mhpmulcl  22170  psdmul  22187  coe1mul2  22287  pmatcoe1fsupp  22722  toponuni  22935  tpsuni  22957  mretopd  23115  neips  23136  neiptoptop  23154  neiptopnei  23155  perflp  23177  perfi  23178  cnf  23269  cnpf  23270  cnpimaex  23279  cnima  23288  t0sep  23347  t1ficld  23350  hausnei  23351  pnrmcld  23365  cnrmi  23383  cmpcov  23412  tgcmp  23424  hauscmplem  23429  connclo  23438  1stcclb  23467  2ndcdisj  23479  llyi  23497  nllyi  23498  ptpjpre1  23594  ptpjcn  23634  ptpjopn  23635  ptclsg  23638  dfac14  23641  txdis1cn  23658  pthaus  23661  hauseqlcld  23669  txkgen  23675  xkococn  23683  txconn  23712  hmeocnvcn  23784  fbssfi  23860  filss  23876  uffixfr  23946  flimneiss  23989  flimelbas  23991  flimfnfcls  24051  alexsubb  24069  alexsubALT  24074  ptcmplem2  24076  ptcmplem3  24077  ptcmplem4  24078  tmdgsum2  24119  ghmcnp  24138  tgpt0  24142  qustgplem  24144  istdrg2  24201  vscacn  24209  tvctdrg  24216  uspreg  24298  ucncn  24309  neipcfilu  24320  cuspcvg  24325  psmetxrge0  24338  isxmet2d  24352  prdsxmetlem  24393  imasdsf1olem  24398  xmstopn  24476  mstopn  24477  stdbdxmet  24543  prdsxmslem2  24557  nrgabv  24697  nmvs  24712  nvclvec  24733  nmoge0  24757  nghmcl  24763  nmoi  24764  nghmghm  24770  nmhmlmhm  24785  nmhmnghm  24786  icccmp  24860  xrge0gsumle  24868  metds0  24885  metdstri  24886  metdsre  24888  metdseq0  24889  metdscnlem  24890  metnrmlem1a  24893  icopnfcnv  24986  xrhmeo  24990  pcoval1  25059  cvslvec  25171  cvsunit  25177  recvs  25192  cphreccllem  25225  cphsscph  25298  cmetcvg  25332  lmle  25348  cmscmet  25393  cmetcusp1  25400  hlcph  25411  minveclem4  25479  ivthlem3  25501  ovolmge0  25525  ovolicc1  25564  ovolicc2lem3  25567  ovolicc2lem5  25569  dyadmbl  25648  i1ff  25724  i1frn  25725  i1fima2  25727  itg2monolem1  25799  dvnres  25981  c1liplem1  26049  c1lip2  26051  dvge0  26059  lhop1lem  26066  itgsubstlem  26103  fta1glem2  26222  fta1b  26225  idomrootle  26226  plyf  26251  plypf1  26265  plyadd  26270  plymul  26271  coeeu  26278  dgrlem  26282  coeid  26291  elqaalem3  26377  aareccl  26382  eff1olem  26604  relogf1o  26622  logdmn0  26696  logcnlem2  26699  logcnlem3  26700  efopnlem1  26712  efopnlem2  26713  logtayl2  26718  cxpcn3lem  26804  cxpcn3  26805  logbgcd1irr  26851  atandmneg  26963  atandmcj  26966  efiatan2  26974  cosatan  26978  cosatanne0  26979  dvatan  26992  areage0  27020  cxp2lim  27034  jensenlem2  27045  jensen  27046  eldmgm  27079  dmgmaddn0  27080  dmlogdmgm  27081  lgamgulmlem2  27087  lgamgulmlem3  27088  lgamgulmlem5  27090  lgambdd  27094  lgamucov  27095  ftalem3  27132  efnnfsumcl  27160  efchtdvds  27216  sqff1o  27239  fsumdvdsdiaglem  27240  dvdsppwf1o  27243  dvdsflf1o  27244  musum  27248  muinv  27250  mpodvdsmulf1o  27251  dvdsmulf1o  27253  lgsfle1  27364  lgsle1  27370  lgsdirprm  27389  lgsne0  27393  lgseisenlem3  27435  lgseisenlem4  27436  lgsquadlem1  27438  lgsquadlem2  27439  chebbnd1  27530  chtppilim  27533  chpchtlim  27537  chpo1ub  27538  dchrmusumlema  27551  dchrvmasumlem1  27553  dchrisum0lema  27572  dchrisum0lem2a  27575  logsqvma  27600  selberg3lem2  27616  pntrsumo1  27623  pnt2  27671  ostthlem1  27685  ostth3  27696  sltval2  27715  addsproplem2  28017  sleadd1  28036  negsid  28087  precsexlem8  28252  precsexlem9  28253  precsexlem11  28255  elons2  28295  sltonold  28297  onscutleft  28299  axtgcgrrflx  28484  axtgcgrid  28485  axtgsegcon  28486  axtg5seg  28487  axtgbtwnid  28488  axtgpasch  28489  axtgcont1  28490  tglng  28568  axcontlem7  28999  axcontlem10  29002  upgrle  29121  umgredg2  29131  lfgredgge2  29155  usgredg2ALT  29224  usgr1vr  29286  usgrexmpledg  29293  upgrres1  29344  fusgrvtxfi  29350  vtxnbuvtx  29422  cusgrcplgr  29451  vdumgr0  29512  vtxdgoddnumeven  29585  trlres  29732  usgr2pth  29796  cyclispthon  29833  clwwlknlen  30060  clwwnonrepclwwnon  30373  2clwwlk2  30376  ablocom  30576  phpar2  30851  cbncms  30893  hlph  30917  hcaucvg  31214  hlimconvi  31219  shaddcl  31245  shmulcl  31246  chlimi  31262  chcompl  31270  choc1  31355  nmopre  31898  cnopc  31941  lnopl  31942  unop  31943  hmop  31950  cnfnc  31958  lnfnl  31959  nlelshi  32088  cnlnadjlem5  32099  elpjidm  32212  mdslle1i  32345  mdslle2i  32346  atcv0  32370  chpssati  32391  aciunf1lem  32678  padct  32736  ssnnssfz  32795  ccatf1  32917  swrdrndisj  32926  ressprs  32938  resspos  32940  resstos  32941  pwrssmgc  32974  ogrpinv0le  33074  ogrpsub  33075  ogrpaddlt  33076  wrdpmtrlast  33095  cyc3evpm  33152  cycpmgcl  33155  cycpmconjslem2  33157  cyc3conja  33159  isarchi3  33176  archirng  33177  archirngz  33178  archiabllem1a  33180  archiabllem1b  33181  archiabllem2a  33183  archiabllem2c  33184  archiabllem2b  33185  archiabl  33187  elrgspnlem1  33231  elrgspnlem2  33232  elrgspnlem4  33234  isdrng4  33278  orngsqr  33313  ornglmulle  33314  orngrmulle  33315  ofldtos  33320  ofldlt1  33322  ofldchr  33323  suborng  33324  subofld  33325  isarchiofld  33326  nn0omnd  33352  quslsm  33412  nsgmgclem  33418  nsgmgc  33419  prmidl0  33457  qsidomlem1  33459  mxidlirred  33479  krull  33486  ufdprmidl  33548  1arithufdlem4  33554  sradrng  33612  extdg1id  33690  ply1annnr  33710  madjusmdetlem4  33790  qtophaus  33796  crefi  33807  cmpcref  33810  cmppcmp  33818  pcmplfin  33820  zart0  33839  tpr2rico  33872  rge0scvg  33909  zrhunitpreima  33938  qqhrhm  33951  esummono  34034  gsumesum  34039  esumrnmpt2  34048  esumpinfval  34053  esumpcvgval  34058  esumpmono  34059  0elsiga  34094  sigaclcu  34097  issgon  34103  inelpisys  34134  ldsysgenld  34140  ldgenpisyslem1  34143  sxuni  34173  isrnmeas  34180  measvuni  34194  measssd  34195  ddemeas  34216  imambfm  34243  elmbfmvol2  34248  dya2icoseg2  34259  omssubaddlem  34280  omssubadd  34281  carsgsigalem  34296  pmeasmono  34305  sibfinima  34320  oddpwdc  34335  oddpwdcv  34336  eulerpartlemf  34351  eulerpartlemt  34352  eulerpartlemr  34355  eulerpartlemgvv  34357  eulerpartlemgs2  34361  fiblem  34379  probtot  34393  ballotlem4  34479  ballotlem5  34480  ballotlemfrc  34507  ballotlemirc  34512  ballotth  34518  hgt750lemb  34649  bnj642  34740  bnj643  34741  bnj645  34742  bnj707  34747  bnj1379  34822  bnj1538  34847  bnj110  34850  bnj93  34855  bnj906  34922  bnj1006  34952  bnj1110  34974  bnj1121  34977  bnj1204  35004  bnj1321  35019  bnj1364  35020  bnj1398  35026  bnj1450  35042  bnj1312  35050  bnj1501  35059  bnj1523  35063  0nn0m1nnn0  35096  subfacp1lem3  35166  subfacp1lem5  35168  pconncn  35208  connpconn  35219  cvmcov  35247  cvmliftlem1  35269  cvmliftlem10  35278  cvmlift2lem11  35297  cvmlift2lem12  35298  msubff1  35540  mvhf1  35543  mthmpps  35566  mclspps  35568  fundmpss  35747  funpartfun  35924  fnetg  36327  neibastop1  36341  filnetlem3  36362  onint1  36431  weiunlem2  36445  weiunpo  36447  weiunse  36450  bj-nnfa  36710  bj-idres  37142  bj-rvecrr  37279  icorempo  37333  pibt2  37399  wl-nfeqfb  37516  phpreu  37590  fin2solem  37592  fin2so  37593  lindsenlbs  37601  matunitlindflem1  37602  matunitlindflem2  37603  matunitlindf  37604  ptrest  37605  poimirlem1  37607  poimirlem2  37608  poimirlem3  37609  poimirlem4  37610  poimirlem5  37611  poimirlem6  37612  poimirlem7  37613  poimirlem8  37614  poimirlem9  37615  poimirlem10  37616  poimirlem11  37617  poimirlem12  37618  poimirlem13  37619  poimirlem14  37620  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem18  37624  poimirlem19  37625  poimirlem20  37626  poimirlem21  37627  poimirlem22  37628  poimirlem23  37629  poimirlem24  37630  poimirlem26  37632  poimirlem27  37633  poimirlem29  37635  poimirlem31  37637  mblfinlem2  37644  dvtan  37656  itg2gt0cn  37661  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  cover2  37701  indexa  37719  istotbnd3  37757  sstotbnd2  37760  sstotbnd  37761  totbndss  37763  equivtotbnd  37764  isbnd3  37770  totbndbnd  37775  equivbnd  37776  prdsbnd  37779  prdstotbnd  37780  heibor  37807  zrdivrng  37939  crngocom  37987  isfld2  37991  dmncrng  38042  eqvrelrel  38578  disjrel  38711  disjdmqscossss  38784  prter2  38862  toycom  38954  lsateln0  38976  lpssat  38994  lssat  38997  oposlem  39163  olop  39195  omllaw  39224  cvlexch1  39309  dihpN  41318  mapdordlem2  41619  linvh  42077  idomnnzpownz  42113  idomnnzgmulnz  42114  aks6d1c5lem2  42119  deg1pow  42122  redvmptabs  42368  readvrec2  42369  readvrec  42370  mhphflem  42582  prjspertr  42591  nacsfg  42692  nacsfix  42699  mzpindd  42733  diophrw  42746  diophrex  42762  rexzrexnn0  42791  pell1234qrdich  42848  rmspecnonsq  42894  rmspecfund  42896  rmspecpos  42904  monotoddzzfi  42930  ltrmxnn0  42937  rmxnn  42939  jm2.23  42984  jm3.1lem2  43006  dnnumch3  43035  lnmlssfg  43068  lnmlmic  43076  lnrlnm  43101  lnr2i  43104  lpirlnr  43105  hbtlem6  43117  hbt  43118  mnccoe  43126  proot1mul  43182  proot1hash  43183  deg1mhm  43188  ondif1i  43251  limnsuc  43254  cantnfresb  43313  succlg  43317  ntrneifv2  44069  grucollcld  44255  mnurndlem1  44276  ismnushort  44296  radcnvrat  44309  binomcxplemdvbinom  44348  binomcxplemcvg  44349  binomcxplemnotnn0  44351  ordelordALT  44534  2uasbanh  44558  ordelordALTVD  44864  elixpconstg  45028  rabidim2  45041  disjinfi  45134  supminfxr2  45418  sumnnodd  45585  stoweidlem7  45962  stoweidlem14  45969  stoweidlem16  45971  stoweidlem24  45979  stoweidlem31  45986  stoweidlem54  46009  wallispilem3  46022  fourierdlem42  46104  fourierdlem48  46109  fourierdlem51  46112  fourierdlem64  46125  fourierdlem76  46137  fourierdlem79  46140  fourierdlem81  46142  fourierdlem87  46148  etransclem28  46217  etransclem32  46221  sge0fodjrnlem  46371  hoidmvlelem3  46552  ovolval5lem3  46609  pimrecltpos  46663  pimrecltneg  46679  issmflem  46682  smfaddlem1  46718  smfsuplem1  46766  smfsuplem3  46768  smflimsuplem7  46781  smfliminflem  46785  tworepnotupword  46839  nfunsnafv  47091  faovcl  47149  tz6.12-2-afv2  47186  tz6.12i-afv2  47192  sprel  47408  evendiv2z  47556  oddp1div2z  47557  2dvdseven  47577  2ndvdsodd  47579  perfectALTVlem1  47645  sbgoldbm  47708  uhgrimisgrgric  47836  clintopcllaw  48054  uzlidlring  48078  rngccatidALTV  48115  funcringcsetcALTV2lem7  48139  ringccatidALTV  48149  ringcinvALTV  48153  funcringcsetclem7ALTV  48162  fldhmsubcALTV  48176  ssnn0ssfz  48193  el0ldepsnzr  48312  regt1loggt0  48385  elbigodm  48404  fllogbd  48409  rrx2xpref1o  48567  unilbss  48665  fdomne0  48679  f002  48683  thincmo2  48827  thincmoALT  48829  fullthinc  48845  elsetrecslem  48929