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  3346  pssne  4040  pssn2lp  4045  ssnpss  4047  eldifn  4073  elinel2  4143  rabsnt  4676  eldifsni  4736  unimax  4888  ssintub  4909  moop2  5457  pwssun  5523  weso  5622  opelxp2  5674  predpo  6288  frpoinsg  6308  ordwe  6337  funmo  6515  funopg  6533  funun  6545  fununi  6574  funimaexg  6586  fndm  6602  frn  6676  f1ss  6742  f1ssr  6743  forn  6756  f1f1orn  6792  f1orescnv  6796  f1imacnv  6797  funcocnv2  6806  dffv2  6936  exfo  7058  foelrn  7060  foelrnf  7061  isorel  7281  isoini2  7294  f1ofveu  7361  fovcld  7494  onminesb  7747  onminsb  7748  tfisg  7805  tfis  7806  limomss  7822  nnlim  7831  ssnlim  7837  resf1ext2b  7886  curry1  8054  curry2  8057  f1o2ndf1  8072  fnwelem  8081  mpoxopn0yelv  8163  tz7.48lem  8380  dif20el  8440  oeordi  8523  oeeulem  8537  oeeui  8538  nnawordex  8573  swoer  8675  eceqoveq  8769  mapsnconst  8840  resixpfo  8884  boxcutc  8889  sdomnen  8928  en0  8965  en0ALT  8966  en0r  8967  en1  8971  dom0  9043  fodomr  9066  dif1enlem  9094  unxpdomlem3  9168  fineqvlem  9176  infn0  9212  fodomfir  9238  f1opwfi  9266  fsuppcolem  9314  fsuppco  9315  mapfienlem1  9318  mapfienlem2  9319  supub  9372  suplub  9373  ordtypelem2  9434  ordtypelem3  9435  ordtypelem6  9438  ordtypelem7  9439  wemapso2lem  9467  wdom2d  9495  brwdom3  9497  ixpiunwdom  9505  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  12870  1nuz2  12874  zsupss  12887  rpgt0  12955  ixxss1  13316  ixxss2  13317  ixxss12  13318  lbioo  13329  ubioo  13330  iccss2  13370  iccssico2  13373  elfzuz3  13475  serge0  14018  expge0  14060  expge1  14061  expaddzlem  14067  hashrabsn1  14336  hashfun  14399  cshinj  14773  relexpuzrel  15014  shftfn  15035  01sqrexlem6  15209  rlimss  15464  lo1dm  15481  o1dm  15492  rlimrege0  15541  fsumf1o  15685  fsumge0  15758  incexc2  15803  supcvg  15821  fprodf1o  15911  divalglem9  16370  bitsfzolem  16403  bitsf1  16415  gcdcllem1  16468  bezout  16512  nprm  16657  dvdsprm  16673  coprm  16681  dfphi2  16744  phimullem  16749  phisum  16761  expnprm  16873  prmreclem2  16888  prmreclem5  16891  1arith  16898  4sqlem18  16933  vdwnnlem3  16968  ramtlecl  16971  rami  16986  0ram  16991  ramub1lem1  16997  prmgaplem5  17026  acsfiel  17620  isacs1i  17623  catlid  17649  catrid  17650  fullfo  17881  fthf1  17886  fthoppc  17892  invfuc  17944  prslem  18263  oduprs  18266  posi  18283  tleile  18385  resspos  18395  resstos  18396  dlatmjdi  18489  pslem  18538  tsrlin  18551  cnvtsr  18554  tsrdir  18570  mndid  18712  mhmf  18757  mhmlin  18761  mhm0  18762  mndind  18796  grpinvex  18919  grplinv  18965  mulgz  19078  mulgdirlem  19081  mulgdir  19082  mulgass  19087  nsgbi  19132  nmzbi  19139  ghmf  19195  ghmlin  19196  conjnsg  19229  gimf1o  19238  gagrpid  19269  gaf  19270  gaass  19272  psgnunilem5  19469  odid  19513  odf1o2  19548  gexid  19556  sylow1lem4  19576  pj1id  19674  efgredeu  19727  ablcmn  19762  cmncom  19773  mulgdi  19801  torsubg  19829  cyggenod2  19860  cygctb  19867  ghmcyg  19871  dprdf1o  20009  ablfacrplem  20042  ablfaclem2  20063  ablfac2  20066  simpg2nsg  20073  fincygsubgodexd  20090  ogrpinv0le  20111  ogrpsub  20112  ogrpaddlt  20113  crngmgp  20222  rnghmmgmhm  20423  rhmmhm  20459  rhmghm  20463  rimf1o  20472  nzrnz  20492  0ringbas  20505  subrgss  20549  subrg1cl  20557  rnghmsubcsetclem1  20608  zrinitorngc  20619  zrtermorngc  20620  rhmsubcsetclem1  20637  ringcinv  20648  zrtermoringc  20652  rrgeq0i  20676  domneq0  20685  domnrrg  20690  drngunit  20711  fldcrngd  20719  drngmgp  20722  drngid  20723  drngdomn  20726  issubdrg  20757  fldhmsubc  20762  fldsdrgfld  20775  cntzsdrg  20779  abvge0  20794  srngcnv  20824  orngsqr  20843  ornglmulle  20844  orngrmulle  20845  ofldtos  20850  ofldlt1  20852  suborng  20853  subofld  20854  lmhmlin  21030  lmimf1o  21058  lvecdrng  21100  lspsolvlem  21140  islbs3  21153  lbsextlem3  21158  2idlelbas  21262  2idlcpblrng  21269  zringunit  21446  prmirredlem  21452  irinitoringc  21459  znidomb  21541  cygzn  21550  ofldchr  21556  psgndiflemB  21580  pjf  21693  frlmsslsp  21776  frlmlbs  21777  f1lindf  21802  assalem  21837  psrbaglefi  21906  psrbagleadd1  21908  mplelsfi  21973  mplsubrglem  21982  mplcoe1  22015  mplbas2  22020  opsrtoslem2  22034  mhpmulcl  22115  psdmul  22132  coe1mul2  22234  pmatcoe1fsupp  22666  toponuni  22879  tpsuni  22901  mretopd  23057  neips  23078  neiptoptop  23096  neiptopnei  23097  perflp  23119  perfi  23120  cnf  23211  cnpf  23212  cnpimaex  23221  cnima  23230  t0sep  23289  t1ficld  23292  hausnei  23293  pnrmcld  23307  cnrmi  23325  cmpcov  23354  tgcmp  23366  hauscmplem  23371  connclo  23380  1stcclb  23409  2ndcdisj  23421  llyi  23439  nllyi  23440  ptpjpre1  23536  ptpjcn  23576  ptpjopn  23577  ptclsg  23580  dfac14  23583  txdis1cn  23600  pthaus  23603  hauseqlcld  23611  txkgen  23617  xkococn  23625  txconn  23654  hmeocnvcn  23726  fbssfi  23802  filss  23818  uffixfr  23888  flimneiss  23931  flimelbas  23933  flimfnfcls  23993  alexsubb  24011  alexsubALT  24016  ptcmplem2  24018  ptcmplem3  24019  ptcmplem4  24020  tmdgsum2  24061  ghmcnp  24080  tgpt0  24084  qustgplem  24086  istdrg2  24143  vscacn  24151  tvctdrg  24158  uspreg  24238  ucncn  24249  neipcfilu  24260  cuspcvg  24265  psmetxrge0  24278  isxmet2d  24292  prdsxmetlem  24333  imasdsf1olem  24338  xmstopn  24416  mstopn  24417  stdbdxmet  24480  prdsxmslem2  24494  nrgabv  24626  nmvs  24641  nvclvec  24662  nmoge0  24686  nghmcl  24692  nmoi  24693  nghmghm  24699  nmhmlmhm  24714  nmhmnghm  24715  icccmp  24791  xrge0gsumle  24799  metds0  24816  metdstri  24817  metdsre  24819  metdseq0  24820  metdscnlem  24821  metnrmlem1a  24824  icopnfcnv  24909  xrhmeo  24913  pcoval1  24980  cvslvec  25092  cvsunit  25098  recvs  25113  cphreccllem  25145  cphsscph  25218  cmetcvg  25252  lmle  25268  cmscmet  25313  cmetcusp1  25320  hlcph  25331  minveclem4  25399  ivthlem3  25420  ovolmge0  25444  ovolicc1  25483  ovolicc2lem3  25486  ovolicc2lem5  25488  dyadmbl  25567  i1ff  25643  i1frn  25644  i1fima2  25646  itg2monolem1  25717  dvnres  25898  c1liplem1  25963  c1lip2  25965  dvge0  25973  lhop1lem  25980  itgsubstlem  26015  fta1glem2  26134  fta1b  26137  idomrootle  26138  plyf  26163  plypf1  26177  plyadd  26182  plymul  26183  coeeu  26190  dgrlem  26194  coeid  26203  elqaalem3  26287  aareccl  26292  eff1olem  26512  relogf1o  26530  logdmn0  26604  logcnlem2  26607  logcnlem3  26608  efopnlem1  26620  efopnlem2  26621  logtayl2  26626  cxpcn3lem  26711  cxpcn3  26712  logbgcd1irr  26758  atandmneg  26870  atandmcj  26873  efiatan2  26881  cosatan  26885  cosatanne0  26886  dvatan  26899  areage0  26927  cxp2lim  26940  jensenlem2  26951  jensen  26952  eldmgm  26985  dmgmaddn0  26986  dmlogdmgm  26987  lgamgulmlem2  26993  lgamgulmlem3  26994  lgamgulmlem5  26996  lgambdd  27000  lgamucov  27001  ftalem3  27038  efnnfsumcl  27066  efchtdvds  27122  sqff1o  27145  fsumdvdsdiaglem  27146  dvdsppwf1o  27149  dvdsflf1o  27150  musum  27154  muinv  27156  mpodvdsmulf1o  27157  dvdsmulf1o  27159  lgsfle1  27269  lgsle1  27275  lgsdirprm  27294  lgsne0  27298  lgseisenlem3  27340  lgseisenlem4  27341  lgsquadlem1  27343  lgsquadlem2  27344  chebbnd1  27435  chtppilim  27438  chpchtlim  27442  chpo1ub  27443  dchrmusumlema  27456  dchrvmasumlem1  27458  dchrisum0lema  27477  dchrisum0lem2a  27480  logsqvma  27505  selberg3lem2  27521  pntrsumo1  27528  pnt2  27576  ostthlem1  27590  ostth3  27601  ltsval2  27620  leftlt  27845  rightgt  27846  precsexlem8  28206  precsexlem9  28207  precsexlem11  28209  elons2  28250  onleft  28252  ltonold  28253  oncutleft  28255  oncutlt  28256  zcuts0  28400  axtgcgrrflx  28530  axtgcgrid  28531  axtgsegcon  28532  axtg5seg  28533  axtgbtwnid  28534  axtgpasch  28535  axtgcont1  28536  tglng  28614  axcontlem7  29039  axcontlem10  29042  upgrle  29159  umgredg2  29169  lfgredgge2  29193  usgredg2ALT  29262  usgr1vr  29324  usgrexmpledg  29331  upgrres1  29382  fusgrvtxfi  29388  vtxnbuvtx  29460  cusgrcplgr  29489  vdumgr0  29549  vtxdgoddnumeven  29622  trlres  29767  usgr2pth  29832  cyclispthon  29872  clwwlknlen  30102  clwwnonrepclwwnon  30415  2clwwlk2  30418  ablocom  30619  phpar2  30894  cbncms  30936  hlph  30960  hcaucvg  31257  hlimconvi  31262  shaddcl  31288  shmulcl  31289  chlimi  31305  chcompl  31313  choc1  31398  nmopre  31941  cnopc  31984  lnopl  31985  unop  31986  hmop  31993  cnfnc  32001  lnfnl  32002  nlelshi  32131  cnlnadjlem5  32142  elpjidm  32255  mdslle1i  32388  mdslle2i  32389  atcv0  32413  aciunf1lem  32735  padct  32791  ssnnssfz  32860  ccatf1  33009  swrdrndisj  33017  ressprs  33026  pwrssmgc  33060  wrdpmtrlast  33154  cyc3evpm  33211  cycpmgcl  33214  cycpmconjslem2  33216  cyc3conja  33218  isarchi3  33248  archirng  33249  archirngz  33250  archiabllem1a  33252  archiabllem1b  33253  archiabllem2a  33255  archiabllem2c  33256  archiabllem2b  33257  archiabl  33259  isarchiofld  33260  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem4  33306  elrgspnsubrun  33310  isdrng4  33356  nn0omnd  33404  quslsm  33465  nsgmgclem  33471  nsgmgc  33472  prmidl0  33510  qsidomlem1  33512  mxidlirred  33532  krull  33539  ufdprmidl  33601  1arithufdlem4  33607  extvfvcl  33680  mplvrpmlem  33687  mplvrpmga  33689  sradrng  33726  extdg1id  33810  ply1annnr  33847  madjusmdetlem4  33974  qtophaus  33980  crefi  33991  cmpcref  33994  cmppcmp  34002  pcmplfin  34004  zart0  34023  tpr2rico  34056  rge0scvg  34093  zrhunitpreima  34120  qqhrhm  34133  esummono  34198  gsumesum  34203  esumrnmpt2  34212  esumpinfval  34217  esumpcvgval  34222  esumpmono  34223  0elsiga  34258  sigaclcu  34261  issgon  34267  inelpisys  34298  ldsysgenld  34304  ldgenpisyslem1  34307  sxuni  34337  isrnmeas  34344  measvuni  34358  measssd  34359  ddemeas  34380  imambfm  34406  elmbfmvol2  34411  dya2icoseg2  34422  omssubaddlem  34443  omssubadd  34444  carsgsigalem  34459  pmeasmono  34468  sibfinima  34483  oddpwdc  34498  oddpwdcv  34499  eulerpartlemf  34514  eulerpartlemt  34515  eulerpartlemr  34518  eulerpartlemgvv  34520  eulerpartlemgs2  34524  fiblem  34542  probtot  34556  ballotlem4  34643  ballotlem5  34644  ballotlemfrc  34671  ballotlemirc  34676  ballotth  34682  hgt750lemb  34800  bnj642  34891  bnj643  34892  bnj645  34893  bnj707  34898  bnj1379  34972  bnj1538  34997  bnj110  35000  bnj93  35005  bnj906  35072  bnj1006  35102  bnj1110  35124  bnj1121  35127  bnj1204  35154  bnj1321  35169  bnj1364  35170  bnj1398  35176  bnj1450  35192  bnj1312  35200  bnj1501  35209  bnj1523  35213  tz9.1regs  35278  0nn0m1nnn0  35295  subfacp1lem3  35364  subfacp1lem5  35366  pconncn  35406  connpconn  35417  cvmcov  35445  cvmliftlem1  35467  cvmliftlem10  35476  cvmlift2lem11  35495  cvmlift2lem12  35496  msubff1  35738  mvhf1  35741  mthmpps  35764  mclspps  35766  fundmpss  35949  funpartfun  36125  fnetg  36527  neibastop1  36541  filnetlem3  36562  onint1  36631  weiunlem  36645  weiunpo  36647  weiunse  36650  bj-nnfa  37025  bj-idres  37474  bj-rvecrr  37611  icorempo  37667  pibt2  37733  wl-nfeqfb  37861  phpreu  37925  fin2solem  37927  fin2so  37928  lindsenlbs  37936  matunitlindflem1  37937  matunitlindflem2  37938  matunitlindf  37939  ptrest  37940  poimirlem1  37942  poimirlem2  37943  poimirlem3  37944  poimirlem4  37945  poimirlem5  37946  poimirlem6  37947  poimirlem7  37948  poimirlem8  37949  poimirlem9  37950  poimirlem10  37951  poimirlem11  37952  poimirlem12  37953  poimirlem13  37954  poimirlem14  37955  poimirlem15  37956  poimirlem16  37957  poimirlem17  37958  poimirlem18  37959  poimirlem19  37960  poimirlem20  37961  poimirlem21  37962  poimirlem22  37963  poimirlem23  37964  poimirlem24  37965  poimirlem26  37967  poimirlem27  37968  poimirlem29  37970  poimirlem31  37972  mblfinlem2  37979  dvtan  37991  itg2gt0cn  37996  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  cover2  38036  indexa  38054  istotbnd3  38092  sstotbnd2  38095  sstotbnd  38096  totbndss  38098  equivtotbnd  38099  isbnd3  38105  totbndbnd  38110  equivbnd  38111  prdsbnd  38114  prdstotbnd  38115  heibor  38142  zrdivrng  38274  crngocom  38322  isfld2  38326  dmncrng  38377  eqvrelrel  39002  disjrel  39151  disjdmqscossss  39227  prter2  39327  toycom  39419  lsateln0  39441  lpssat  39459  lssat  39462  oposlem  39628  olop  39660  omllaw  39689  cvlexch1  39774  dihpN  41782  mapdordlem2  42083  linvh  42535  idomnnzpownz  42571  idomnnzgmulnz  42572  aks6d1c5lem2  42577  deg1pow  42580  redvmptabs  42792  readvrec2  42793  readvrec  42794  mhphflem  43029  prjspertr  43038  nacsfg  43137  nacsfix  43144  mzpindd  43178  diophrw  43191  diophrex  43207  rexzrexnn0  43232  pell1234qrdich  43289  rmspecnonsq  43335  rmspecfund  43337  rmspecpos  43344  monotoddzzfi  43370  ltrmxnn0  43377  rmxnn  43379  jm2.23  43424  jm3.1lem2  43446  dnnumch3  43475  lnmlssfg  43508  lnmlmic  43516  lnrlnm  43541  lnr2i  43544  lpirlnr  43545  hbtlem6  43557  hbt  43558  mnccoe  43566  proot1mul  43622  proot1hash  43623  deg1mhm  43628  ondif1i  43690  limnsuc  43693  cantnfresb  43752  succlg  43756  ntrneifv2  44507  grucollcld  44687  mnurndlem1  44708  ismnushort  44728  radcnvrat  44741  binomcxplemdvbinom  44780  binomcxplemcvg  44781  binomcxplemnotnn0  44783  ordelordALT  44964  2uasbanh  44988  ordelordALTVD  45293  relprel  45378  elixpconstg  45519  rabidim2  45532  disjinfi  45622  supminfxr2  45897  sumnnodd  46060  stoweidlem7  46435  stoweidlem14  46442  stoweidlem16  46444  stoweidlem24  46452  stoweidlem31  46459  stoweidlem54  46482  wallispilem3  46495  fourierdlem42  46577  fourierdlem48  46582  fourierdlem51  46585  fourierdlem64  46598  fourierdlem76  46610  fourierdlem79  46613  fourierdlem81  46615  fourierdlem87  46621  etransclem28  46690  etransclem32  46694  sge0fodjrnlem  46844  hoidmvlelem3  47025  ovolval5lem3  47082  pimrecltpos  47136  pimrecltneg  47152  issmflem  47155  smfaddlem1  47191  smfsuplem1  47239  smfsuplem3  47241  smflimsuplem7  47254  smfliminflem  47258  nfunsnafv  47584  faovcl  47642  tz6.12-2-afv2  47679  tz6.12i-afv2  47685  sprel  47938  evendiv2z  48102  oddp1div2z  48103  2dvdseven  48123  2ndvdsodd  48125  perfectALTVlem1  48191  sbgoldbm  48254  upgrimtrls  48376  upgrimpthslem1  48377  upgrimspths  48380  upgrimcycls  48381  uhgrimisgrgric  48401  gpgprismgr4cycllem2  48566  clintopcllaw  48681  uzlidlring  48705  rngccatidALTV  48742  funcringcsetcALTV2lem7  48766  ringccatidALTV  48776  ringcinvALTV  48780  funcringcsetclem7ALTV  48789  fldhmsubcALTV  48803  ssnn0ssfz  48819  el0ldepsnzr  48937  regt1loggt0  49006  elbigodm  49025  fllogbd  49030  rrx2xpref1o  49188  unilbss  49287  fdomne0  49319  f002  49323  xpco2  49326  imaf1homlem  49576  idemb  49628  uobeq2  49870  thincmo2  49895  thincmoALT  49898  fullthinc  49919  idfudiag1  49994  elsetrecslem  50168