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  1519  eumo  2577  reurmo  3362  pssne  4074  pssn2lp  4079  ssnpss  4081  eldifn  4107  elinel2  4177  rabsnt  4707  eldifsni  4766  unimax  4920  ssintub  4942  moop2  5477  pwssun  5545  weso  5645  opelxp2  5697  predpo  6312  frpoinsg  6332  wfisgOLD  6343  ordwe  6365  funmo  6550  funmoOLD  6551  funopg  6569  funun  6581  fununi  6610  funimaexg  6622  fndm  6640  frn  6712  f1ss  6778  f1ssr  6779  forn  6792  f1f1orn  6828  f1orescnv  6832  f1imacnv  6833  funcocnv2  6842  dffv2  6973  exfo  7094  foelrn  7096  foelrnf  7097  isorel  7318  isoini2  7331  f1ofveu  7397  fovcld  7532  onminesb  7785  onminsb  7786  tfisg  7847  tfis  7848  limomss  7864  nnlim  7873  ssnlim  7879  resf1ext2b  7929  curry1  8101  curry2  8104  f1o2ndf1  8119  fnwelem  8128  mpoxopn0yelv  8210  wfrlem5OLD  8325  tz7.48lem  8453  dif20el  8515  oeordi  8597  oeeulem  8611  oeeui  8612  nnawordex  8647  swoer  8748  eceqoveq  8834  mapsnconst  8904  resixpfo  8948  boxcutc  8953  sdomnen  8993  en0  9030  en0ALT  9031  en0r  9032  en1  9036  dom0  9114  fodomr  9140  dif1enlem  9168  dif1enlemOLD  9169  unxpdomlem3  9258  fineqvlem  9268  infn0  9310  fodomfir  9338  f1opwfi  9366  fsuppcolem  9411  fsuppco  9412  mapfienlem1  9415  mapfienlem2  9416  supub  9469  suplub  9470  ordtypelem2  9531  ordtypelem3  9532  ordtypelem6  9535  ordtypelem7  9536  wemapso2lem  9564  wdom2d  9592  brwdom3  9594  ixpiunwdom  9602  inf3lem2  9641  inf3lem6  9645  oancom  9663  infdifsn  9669  cantnfp1lem3  9692  cantnflem3  9703  cantnflem4  9704  oef1o  9710  cnfcom3  9716  tctr  9752  frinsg  9763  tz9.12lem3  9801  scottex  9897  cardid2  9965  infxpenlem  10025  acni3  10059  cardaleph  10101  iscard3  10105  dfac5lem4  10138  dfac5lem5  10139  dfac5lem4OLD  10140  kmlem1  10163  cofsmo  10281  fin4en1  10321  enfin2i  10333  fin23lem28  10352  fin23lem38  10361  isf32lem6  10370  enfin1ai  10396  hsmexlem2  10439  hsmexlem4  10441  domtriomlem  10454  axdc2lem  10460  axdc3lem2  10463  ac6num  10491  zorn2lem2  10509  brdom3  10540  alephval2  10584  alephreg  10594  pwcfsdom  10595  smobeth  10598  fpwwe2lem5  10647  fpwwe2lem12  10654  canthp1lem2  10665  pwfseqlem3  10672  hargch  10685  winalim2  10708  gchina  10711  inar1  10787  0npi  10894  mulclpi  10905  mulcanpi  10912  nlt1pi  10918  nqereu  10941  prcdnq  11005  prnmax  11007  ltresr2  11153  axrnegex  11174  axpre-sup  11181  eluz2gt1  12934  1nuz2  12938  zsupss  12951  rpgt0  13019  ixxss1  13378  ixxss2  13379  ixxss12  13380  lbioo  13391  ubioo  13392  iccss2  13432  iccssico2  13435  elfzuz3  13536  serge0  14072  expge0  14114  expge1  14115  expaddzlem  14121  hashrabsn1  14390  hashfun  14453  cshinj  14827  relexpuzrel  15069  shftfn  15090  01sqrexlem6  15264  rlimss  15516  lo1dm  15533  o1dm  15544  rlimrege0  15593  fsumf1o  15737  fsumge0  15809  incexc2  15852  supcvg  15870  fprodf1o  15960  divalglem9  16418  bitsfzolem  16451  bitsf1  16463  gcdcllem1  16516  bezout  16560  nprm  16705  dvdsprm  16720  coprm  16728  dfphi2  16791  phimullem  16796  phisum  16808  expnprm  16920  prmreclem2  16935  prmreclem5  16938  1arith  16945  4sqlem18  16980  vdwnnlem3  17015  ramtlecl  17018  rami  17033  0ram  17038  ramub1lem1  17044  prmgaplem5  17073  acsfiel  17664  isacs1i  17667  catlid  17693  catrid  17694  fullfo  17925  fthf1  17930  fthoppc  17936  invfuc  17988  prslem  18307  oduprs  18310  posi  18327  tleile  18429  dlatmjdi  18531  pslem  18580  tsrlin  18593  cnvtsr  18596  tsrdir  18612  mndid  18720  mhmf  18765  mhmlin  18769  mhm0  18770  mndind  18804  grpinvex  18924  grplinv  18970  mulgz  19083  mulgdirlem  19086  mulgdir  19087  mulgass  19092  nsgbi  19138  nmzbi  19145  ghmf  19201  ghmlin  19202  conjnsg  19235  gimf1o  19244  gagrpid  19275  gaf  19276  gaass  19278  psgnunilem5  19473  odid  19517  odf1o2  19552  gexid  19560  sylow1lem4  19580  pj1id  19678  efgredeu  19731  ablcmn  19766  cmncom  19777  mulgdi  19805  torsubg  19833  cyggenod2  19864  cygctb  19871  ghmcyg  19875  dprdf1o  20013  ablfacrplem  20046  ablfaclem2  20067  ablfac2  20070  simpg2nsg  20077  fincygsubgodexd  20094  crngmgp  20199  rnghmmgmhm  20401  rhmmhm  20437  rhmghm  20442  rimf1o  20452  nzrnz  20473  0ringbas  20486  subrgss  20530  subrg1cl  20538  rnghmsubcsetclem1  20589  zrinitorngc  20600  zrtermorngc  20601  rhmsubcsetclem1  20618  ringcinv  20629  zrtermoringc  20633  rrgeq0i  20657  domneq0  20666  domnrrg  20671  drngunit  20692  fldcrngd  20700  drngmgp  20703  drngid  20704  drngdomn  20707  issubdrg  20738  fldhmsubc  20743  fldsdrgfld  20756  cntzsdrg  20760  abvge0  20775  srngcnv  20805  lmhmlin  20991  lmimf1o  21019  lvecdrng  21061  lspsolvlem  21101  islbs3  21114  lbsextlem3  21119  2idlelbas  21223  2idlcpblrng  21230  zringunit  21425  prmirredlem  21431  irinitoringc  21438  znidomb  21520  cygzn  21529  psgndiflemB  21558  pjf  21671  frlmsslsp  21754  frlmlbs  21755  f1lindf  21780  assalem  21815  psrbaglefi  21884  psrbagleadd1  21886  mplelsfi  21953  mplsubrglem  21962  mplcoe1  21993  mplbas2  21998  opsrtoslem2  22012  mhpmulcl  22085  psdmul  22102  coe1mul2  22204  pmatcoe1fsupp  22637  toponuni  22850  tpsuni  22872  mretopd  23028  neips  23049  neiptoptop  23067  neiptopnei  23068  perflp  23090  perfi  23091  cnf  23182  cnpf  23183  cnpimaex  23192  cnima  23201  t0sep  23260  t1ficld  23263  hausnei  23264  pnrmcld  23278  cnrmi  23296  cmpcov  23325  tgcmp  23337  hauscmplem  23342  connclo  23351  1stcclb  23380  2ndcdisj  23392  llyi  23410  nllyi  23411  ptpjpre1  23507  ptpjcn  23547  ptpjopn  23548  ptclsg  23551  dfac14  23554  txdis1cn  23571  pthaus  23574  hauseqlcld  23582  txkgen  23588  xkococn  23596  txconn  23625  hmeocnvcn  23697  fbssfi  23773  filss  23789  uffixfr  23859  flimneiss  23902  flimelbas  23904  flimfnfcls  23964  alexsubb  23982  alexsubALT  23987  ptcmplem2  23989  ptcmplem3  23990  ptcmplem4  23991  tmdgsum2  24032  ghmcnp  24051  tgpt0  24055  qustgplem  24057  istdrg2  24114  vscacn  24122  tvctdrg  24129  uspreg  24210  ucncn  24221  neipcfilu  24232  cuspcvg  24237  psmetxrge0  24250  isxmet2d  24264  prdsxmetlem  24305  imasdsf1olem  24310  xmstopn  24388  mstopn  24389  stdbdxmet  24452  prdsxmslem2  24466  nrgabv  24598  nmvs  24613  nvclvec  24634  nmoge0  24658  nghmcl  24664  nmoi  24665  nghmghm  24671  nmhmlmhm  24686  nmhmnghm  24687  icccmp  24763  xrge0gsumle  24771  metds0  24788  metdstri  24789  metdsre  24791  metdseq0  24792  metdscnlem  24793  metnrmlem1a  24796  icopnfcnv  24889  xrhmeo  24893  pcoval1  24962  cvslvec  25074  cvsunit  25080  recvs  25095  cphreccllem  25128  cphsscph  25201  cmetcvg  25235  lmle  25251  cmscmet  25296  cmetcusp1  25303  hlcph  25314  minveclem4  25382  ivthlem3  25404  ovolmge0  25428  ovolicc1  25467  ovolicc2lem3  25470  ovolicc2lem5  25472  dyadmbl  25551  i1ff  25627  i1frn  25628  i1fima2  25630  itg2monolem1  25701  dvnres  25883  c1liplem1  25951  c1lip2  25953  dvge0  25961  lhop1lem  25968  itgsubstlem  26005  fta1glem2  26124  fta1b  26127  idomrootle  26128  plyf  26153  plypf1  26167  plyadd  26172  plymul  26173  coeeu  26180  dgrlem  26184  coeid  26193  elqaalem3  26279  aareccl  26284  eff1olem  26507  relogf1o  26525  logdmn0  26599  logcnlem2  26602  logcnlem3  26603  efopnlem1  26615  efopnlem2  26616  logtayl2  26621  cxpcn3lem  26707  cxpcn3  26708  logbgcd1irr  26754  atandmneg  26866  atandmcj  26869  efiatan2  26877  cosatan  26881  cosatanne0  26882  dvatan  26895  areage0  26923  cxp2lim  26937  jensenlem2  26948  jensen  26949  eldmgm  26982  dmgmaddn0  26983  dmlogdmgm  26984  lgamgulmlem2  26990  lgamgulmlem3  26991  lgamgulmlem5  26993  lgambdd  26997  lgamucov  26998  ftalem3  27035  efnnfsumcl  27063  efchtdvds  27119  sqff1o  27142  fsumdvdsdiaglem  27143  dvdsppwf1o  27146  dvdsflf1o  27147  musum  27151  muinv  27153  mpodvdsmulf1o  27154  dvdsmulf1o  27156  lgsfle1  27267  lgsle1  27273  lgsdirprm  27292  lgsne0  27296  lgseisenlem3  27338  lgseisenlem4  27339  lgsquadlem1  27341  lgsquadlem2  27342  chebbnd1  27433  chtppilim  27436  chpchtlim  27440  chpo1ub  27441  dchrmusumlema  27454  dchrvmasumlem1  27456  dchrisum0lema  27475  dchrisum0lem2a  27478  logsqvma  27503  selberg3lem2  27519  pntrsumo1  27526  pnt2  27574  ostthlem1  27588  ostth3  27599  sltval2  27618  addsproplem2  27920  sleadd1  27939  negsid  27990  precsexlem8  28155  precsexlem9  28156  precsexlem11  28158  elons2  28198  sltonold  28200  onscutleft  28202  axtgcgrrflx  28387  axtgcgrid  28388  axtgsegcon  28389  axtg5seg  28390  axtgbtwnid  28391  axtgpasch  28392  axtgcont1  28393  tglng  28471  axcontlem7  28895  axcontlem10  28898  upgrle  29015  umgredg2  29025  lfgredgge2  29049  usgredg2ALT  29118  usgr1vr  29180  usgrexmpledg  29187  upgrres1  29238  fusgrvtxfi  29244  vtxnbuvtx  29316  cusgrcplgr  29345  vdumgr0  29406  vtxdgoddnumeven  29479  trlres  29626  usgr2pth  29692  cyclispthon  29732  clwwlknlen  29959  clwwnonrepclwwnon  30272  2clwwlk2  30275  ablocom  30475  phpar2  30750  cbncms  30792  hlph  30816  hcaucvg  31113  hlimconvi  31118  shaddcl  31144  shmulcl  31145  chlimi  31161  chcompl  31169  choc1  31254  nmopre  31797  cnopc  31840  lnopl  31841  unop  31842  hmop  31849  cnfnc  31857  lnfnl  31858  nlelshi  31987  cnlnadjlem5  31998  elpjidm  32111  mdslle1i  32244  mdslle2i  32245  atcv0  32269  chpssati  32290  aciunf1lem  32586  padct  32643  ssnnssfz  32710  ccatf1  32870  swrdrndisj  32879  ressprs  32890  resspos  32892  resstos  32893  pwrssmgc  32926  ogrpinv0le  33029  ogrpsub  33030  ogrpaddlt  33031  wrdpmtrlast  33050  cyc3evpm  33107  cycpmgcl  33110  cycpmconjslem2  33112  cyc3conja  33114  isarchi3  33131  archirng  33132  archirngz  33133  archiabllem1a  33135  archiabllem1b  33136  archiabllem2a  33138  archiabllem2c  33139  archiabllem2b  33140  archiabl  33142  elrgspnlem1  33183  elrgspnlem2  33184  elrgspnlem4  33186  elrgspnsubrun  33190  isdrng4  33235  orngsqr  33272  ornglmulle  33273  orngrmulle  33274  ofldtos  33279  ofldlt1  33281  ofldchr  33282  suborng  33283  subofld  33284  isarchiofld  33285  nn0omnd  33306  quslsm  33366  nsgmgclem  33372  nsgmgc  33373  prmidl0  33411  qsidomlem1  33413  mxidlirred  33433  krull  33440  ufdprmidl  33502  1arithufdlem4  33508  sradrng  33568  extdg1id  33653  ply1annnr  33683  madjusmdetlem4  33807  qtophaus  33813  crefi  33824  cmpcref  33827  cmppcmp  33835  pcmplfin  33837  zart0  33856  tpr2rico  33889  rge0scvg  33926  zrhunitpreima  33953  qqhrhm  33966  esummono  34031  gsumesum  34036  esumrnmpt2  34045  esumpinfval  34050  esumpcvgval  34055  esumpmono  34056  0elsiga  34091  sigaclcu  34094  issgon  34100  inelpisys  34131  ldsysgenld  34137  ldgenpisyslem1  34140  sxuni  34170  isrnmeas  34177  measvuni  34191  measssd  34192  ddemeas  34213  imambfm  34240  elmbfmvol2  34245  dya2icoseg2  34256  omssubaddlem  34277  omssubadd  34278  carsgsigalem  34293  pmeasmono  34302  sibfinima  34317  oddpwdc  34332  oddpwdcv  34333  eulerpartlemf  34348  eulerpartlemt  34349  eulerpartlemr  34352  eulerpartlemgvv  34354  eulerpartlemgs2  34358  fiblem  34376  probtot  34390  ballotlem4  34477  ballotlem5  34478  ballotlemfrc  34505  ballotlemirc  34510  ballotth  34516  hgt750lemb  34634  bnj642  34725  bnj643  34726  bnj645  34727  bnj707  34732  bnj1379  34807  bnj1538  34832  bnj110  34835  bnj93  34840  bnj906  34907  bnj1006  34937  bnj1110  34959  bnj1121  34962  bnj1204  34989  bnj1321  35004  bnj1364  35005  bnj1398  35011  bnj1450  35027  bnj1312  35035  bnj1501  35044  bnj1523  35048  0nn0m1nnn0  35081  subfacp1lem3  35150  subfacp1lem5  35152  pconncn  35192  connpconn  35203  cvmcov  35231  cvmliftlem1  35253  cvmliftlem10  35262  cvmlift2lem11  35281  cvmlift2lem12  35282  msubff1  35524  mvhf1  35527  mthmpps  35550  mclspps  35552  fundmpss  35730  funpartfun  35907  fnetg  36309  neibastop1  36323  filnetlem3  36344  onint1  36413  weiunlem2  36427  weiunpo  36429  weiunse  36432  bj-nnfa  36692  bj-idres  37124  bj-rvecrr  37261  icorempo  37315  pibt2  37381  wl-nfeqfb  37500  phpreu  37574  fin2solem  37576  fin2so  37577  lindsenlbs  37585  matunitlindflem1  37586  matunitlindflem2  37587  matunitlindf  37588  ptrest  37589  poimirlem1  37591  poimirlem2  37592  poimirlem3  37593  poimirlem4  37594  poimirlem5  37595  poimirlem6  37596  poimirlem7  37597  poimirlem8  37598  poimirlem9  37599  poimirlem10  37600  poimirlem11  37601  poimirlem12  37602  poimirlem13  37603  poimirlem14  37604  poimirlem15  37605  poimirlem16  37606  poimirlem17  37607  poimirlem18  37608  poimirlem19  37609  poimirlem20  37610  poimirlem21  37611  poimirlem22  37612  poimirlem23  37613  poimirlem24  37614  poimirlem26  37616  poimirlem27  37617  poimirlem29  37619  poimirlem31  37621  mblfinlem2  37628  dvtan  37640  itg2gt0cn  37645  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  cover2  37685  indexa  37703  istotbnd3  37741  sstotbnd2  37744  sstotbnd  37745  totbndss  37747  equivtotbnd  37748  isbnd3  37754  totbndbnd  37759  equivbnd  37760  prdsbnd  37763  prdstotbnd  37764  heibor  37791  zrdivrng  37923  crngocom  37971  isfld2  37975  dmncrng  38026  eqvrelrel  38561  disjrel  38694  disjdmqscossss  38767  prter2  38845  toycom  38937  lsateln0  38959  lpssat  38977  lssat  38980  oposlem  39146  olop  39178  omllaw  39207  cvlexch1  39292  dihpN  41301  mapdordlem2  41602  linvh  42055  idomnnzpownz  42091  idomnnzgmulnz  42092  aks6d1c5lem2  42097  deg1pow  42100  redvmptabs  42350  readvrec2  42351  readvrec  42352  mhphflem  42566  prjspertr  42575  nacsfg  42675  nacsfix  42682  mzpindd  42716  diophrw  42729  diophrex  42745  rexzrexnn0  42774  pell1234qrdich  42831  rmspecnonsq  42877  rmspecfund  42879  rmspecpos  42887  monotoddzzfi  42913  ltrmxnn0  42920  rmxnn  42922  jm2.23  42967  jm3.1lem2  42989  dnnumch3  43018  lnmlssfg  43051  lnmlmic  43059  lnrlnm  43084  lnr2i  43087  lpirlnr  43088  hbtlem6  43100  hbt  43101  mnccoe  43109  proot1mul  43165  proot1hash  43166  deg1mhm  43171  ondif1i  43233  limnsuc  43236  cantnfresb  43295  succlg  43299  ntrneifv2  44051  grucollcld  44232  mnurndlem1  44253  ismnushort  44273  radcnvrat  44286  binomcxplemdvbinom  44325  binomcxplemcvg  44326  binomcxplemnotnn0  44328  ordelordALT  44510  2uasbanh  44534  ordelordALTVD  44839  relprel  44924  elixpconstg  45061  rabidim2  45074  disjinfi  45164  supminfxr2  45444  sumnnodd  45607  stoweidlem7  45984  stoweidlem14  45991  stoweidlem16  45993  stoweidlem24  46001  stoweidlem31  46008  stoweidlem54  46031  wallispilem3  46044  fourierdlem42  46126  fourierdlem48  46131  fourierdlem51  46134  fourierdlem64  46147  fourierdlem76  46159  fourierdlem79  46162  fourierdlem81  46164  fourierdlem87  46170  etransclem28  46239  etransclem32  46243  sge0fodjrnlem  46393  hoidmvlelem3  46574  ovolval5lem3  46631  pimrecltpos  46685  pimrecltneg  46701  issmflem  46704  smfaddlem1  46740  smfsuplem1  46788  smfsuplem3  46790  smflimsuplem7  46803  smfliminflem  46807  tworepnotupword  46863  nfunsnafv  47119  faovcl  47177  tz6.12-2-afv2  47214  tz6.12i-afv2  47220  sprel  47446  evendiv2z  47594  oddp1div2z  47595  2dvdseven  47615  2ndvdsodd  47617  perfectALTVlem1  47683  sbgoldbm  47746  upgrimtrls  47867  upgrimpthslem1  47868  upgrimspths  47871  upgrimcycls  47872  uhgrimisgrgric  47892  gpgprismgr4cycllem2  48043  clintopcllaw  48134  uzlidlring  48158  rngccatidALTV  48195  funcringcsetcALTV2lem7  48219  ringccatidALTV  48229  ringcinvALTV  48233  funcringcsetclem7ALTV  48242  fldhmsubcALTV  48256  ssnn0ssfz  48272  el0ldepsnzr  48391  regt1loggt0  48464  elbigodm  48483  fllogbd  48488  rrx2xpref1o  48646  unilbss  48744  fdomne0  48776  f002  48780  imaf1homlem  49014  thincmo2  49260  thincmoALT  49263  fullthinc  49284  idfudiag1  49358  elsetrecslem  49511