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  2571  reurmo  3348  pssne  4052  pssn2lp  4057  ssnpss  4059  eldifn  4085  elinel2  4155  rabsnt  4685  eldifsni  4744  unimax  4897  ssintub  4919  moop2  5449  pwssun  5515  weso  5614  opelxp2  5666  predpo  6275  frpoinsg  6295  ordwe  6324  funmo  6502  funopg  6520  funun  6532  fununi  6561  funimaexg  6573  fndm  6589  frn  6663  f1ss  6729  f1ssr  6730  forn  6743  f1f1orn  6779  f1orescnv  6783  f1imacnv  6784  funcocnv2  6793  dffv2  6922  exfo  7043  foelrn  7045  foelrnf  7046  isorel  7267  isoini2  7280  f1ofveu  7347  fovcld  7480  onminesb  7733  onminsb  7734  tfisg  7794  tfis  7795  limomss  7811  nnlim  7820  ssnlim  7826  resf1ext2b  7875  curry1  8044  curry2  8047  f1o2ndf1  8062  fnwelem  8071  mpoxopn0yelv  8153  tz7.48lem  8370  dif20el  8430  oeordi  8512  oeeulem  8526  oeeui  8527  nnawordex  8562  swoer  8663  eceqoveq  8756  mapsnconst  8826  resixpfo  8870  boxcutc  8875  sdomnen  8913  en0  8950  en0ALT  8951  en0r  8952  en1  8956  dom0  9029  fodomr  9052  dif1enlem  9080  dif1enlemOLD  9081  unxpdomlem3  9157  fineqvlem  9167  infn0  9209  fodomfir  9237  f1opwfi  9265  fsuppcolem  9310  fsuppco  9311  mapfienlem1  9314  mapfienlem2  9315  supub  9368  suplub  9369  ordtypelem2  9430  ordtypelem3  9431  ordtypelem6  9434  ordtypelem7  9435  wemapso2lem  9463  wdom2d  9491  brwdom3  9493  ixpiunwdom  9501  inf3lem2  9544  inf3lem6  9548  oancom  9566  infdifsn  9572  cantnfp1lem3  9595  cantnflem3  9606  cantnflem4  9607  oef1o  9613  cnfcom3  9619  tctr  9655  frinsg  9666  tz9.12lem3  9704  scottex  9800  cardid2  9868  infxpenlem  9926  acni3  9960  cardaleph  10002  iscard3  10006  dfac5lem4  10039  dfac5lem5  10040  dfac5lem4OLD  10041  kmlem1  10064  cofsmo  10182  fin4en1  10222  enfin2i  10234  fin23lem28  10253  fin23lem38  10262  isf32lem6  10271  enfin1ai  10297  hsmexlem2  10340  hsmexlem4  10342  domtriomlem  10355  axdc2lem  10361  axdc3lem2  10364  ac6num  10392  zorn2lem2  10410  brdom3  10441  alephval2  10485  alephreg  10495  pwcfsdom  10496  smobeth  10499  fpwwe2lem5  10548  fpwwe2lem12  10555  canthp1lem2  10566  pwfseqlem3  10573  hargch  10586  winalim2  10609  gchina  10612  inar1  10688  0npi  10795  mulclpi  10806  mulcanpi  10813  nlt1pi  10819  nqereu  10842  prcdnq  10906  prnmax  10908  ltresr2  11054  axrnegex  11075  axpre-sup  11082  eluz2gt1  12839  1nuz2  12843  zsupss  12856  rpgt0  12924  ixxss1  13284  ixxss2  13285  ixxss12  13286  lbioo  13297  ubioo  13298  iccss2  13338  iccssico2  13341  elfzuz3  13442  serge0  13981  expge0  14023  expge1  14024  expaddzlem  14030  hashrabsn1  14299  hashfun  14362  cshinj  14735  relexpuzrel  14977  shftfn  14998  01sqrexlem6  15172  rlimss  15427  lo1dm  15444  o1dm  15455  rlimrege0  15504  fsumf1o  15648  fsumge0  15720  incexc2  15763  supcvg  15781  fprodf1o  15871  divalglem9  16330  bitsfzolem  16363  bitsf1  16375  gcdcllem1  16428  bezout  16472  nprm  16617  dvdsprm  16632  coprm  16640  dfphi2  16703  phimullem  16708  phisum  16720  expnprm  16832  prmreclem2  16847  prmreclem5  16850  1arith  16857  4sqlem18  16892  vdwnnlem3  16927  ramtlecl  16930  rami  16945  0ram  16950  ramub1lem1  16956  prmgaplem5  16985  acsfiel  17578  isacs1i  17581  catlid  17607  catrid  17608  fullfo  17839  fthf1  17844  fthoppc  17850  invfuc  17902  prslem  18221  oduprs  18224  posi  18241  tleile  18343  resspos  18353  resstos  18354  dlatmjdi  18447  pslem  18496  tsrlin  18509  cnvtsr  18512  tsrdir  18528  mndid  18636  mhmf  18681  mhmlin  18685  mhm0  18686  mndind  18720  grpinvex  18840  grplinv  18886  mulgz  18999  mulgdirlem  19002  mulgdir  19003  mulgass  19008  nsgbi  19054  nmzbi  19061  ghmf  19117  ghmlin  19118  conjnsg  19151  gimf1o  19160  gagrpid  19191  gaf  19192  gaass  19194  psgnunilem5  19391  odid  19435  odf1o2  19470  gexid  19478  sylow1lem4  19498  pj1id  19596  efgredeu  19649  ablcmn  19684  cmncom  19695  mulgdi  19723  torsubg  19751  cyggenod2  19782  cygctb  19789  ghmcyg  19793  dprdf1o  19931  ablfacrplem  19964  ablfaclem2  19985  ablfac2  19988  simpg2nsg  19995  fincygsubgodexd  20012  ogrpinv0le  20033  ogrpsub  20034  ogrpaddlt  20035  crngmgp  20144  rnghmmgmhm  20346  rhmmhm  20382  rhmghm  20387  rimf1o  20397  nzrnz  20418  0ringbas  20431  subrgss  20475  subrg1cl  20483  rnghmsubcsetclem1  20534  zrinitorngc  20545  zrtermorngc  20546  rhmsubcsetclem1  20563  ringcinv  20574  zrtermoringc  20578  rrgeq0i  20602  domneq0  20611  domnrrg  20616  drngunit  20637  fldcrngd  20645  drngmgp  20648  drngid  20649  drngdomn  20652  issubdrg  20683  fldhmsubc  20688  fldsdrgfld  20701  cntzsdrg  20705  abvge0  20720  srngcnv  20750  orngsqr  20769  ornglmulle  20770  orngrmulle  20771  ofldtos  20776  ofldlt1  20778  suborng  20779  subofld  20780  lmhmlin  20957  lmimf1o  20985  lvecdrng  21027  lspsolvlem  21067  islbs3  21080  lbsextlem3  21085  2idlelbas  21189  2idlcpblrng  21196  zringunit  21391  prmirredlem  21397  irinitoringc  21404  znidomb  21486  cygzn  21495  ofldchr  21501  psgndiflemB  21525  pjf  21638  frlmsslsp  21721  frlmlbs  21722  f1lindf  21747  assalem  21782  psrbaglefi  21851  psrbagleadd1  21853  mplelsfi  21920  mplsubrglem  21929  mplcoe1  21960  mplbas2  21965  opsrtoslem2  21979  mhpmulcl  22052  psdmul  22069  coe1mul2  22171  pmatcoe1fsupp  22604  toponuni  22817  tpsuni  22839  mretopd  22995  neips  23016  neiptoptop  23034  neiptopnei  23035  perflp  23057  perfi  23058  cnf  23149  cnpf  23150  cnpimaex  23159  cnima  23168  t0sep  23227  t1ficld  23230  hausnei  23231  pnrmcld  23245  cnrmi  23263  cmpcov  23292  tgcmp  23304  hauscmplem  23309  connclo  23318  1stcclb  23347  2ndcdisj  23359  llyi  23377  nllyi  23378  ptpjpre1  23474  ptpjcn  23514  ptpjopn  23515  ptclsg  23518  dfac14  23521  txdis1cn  23538  pthaus  23541  hauseqlcld  23549  txkgen  23555  xkococn  23563  txconn  23592  hmeocnvcn  23664  fbssfi  23740  filss  23756  uffixfr  23826  flimneiss  23869  flimelbas  23871  flimfnfcls  23931  alexsubb  23949  alexsubALT  23954  ptcmplem2  23956  ptcmplem3  23957  ptcmplem4  23958  tmdgsum2  23999  ghmcnp  24018  tgpt0  24022  qustgplem  24024  istdrg2  24081  vscacn  24089  tvctdrg  24096  uspreg  24177  ucncn  24188  neipcfilu  24199  cuspcvg  24204  psmetxrge0  24217  isxmet2d  24231  prdsxmetlem  24272  imasdsf1olem  24277  xmstopn  24355  mstopn  24356  stdbdxmet  24419  prdsxmslem2  24433  nrgabv  24565  nmvs  24580  nvclvec  24601  nmoge0  24625  nghmcl  24631  nmoi  24632  nghmghm  24638  nmhmlmhm  24653  nmhmnghm  24654  icccmp  24730  xrge0gsumle  24738  metds0  24755  metdstri  24756  metdsre  24758  metdseq0  24759  metdscnlem  24760  metnrmlem1a  24763  icopnfcnv  24856  xrhmeo  24860  pcoval1  24929  cvslvec  25041  cvsunit  25047  recvs  25062  cphreccllem  25094  cphsscph  25167  cmetcvg  25201  lmle  25217  cmscmet  25262  cmetcusp1  25269  hlcph  25280  minveclem4  25348  ivthlem3  25370  ovolmge0  25394  ovolicc1  25433  ovolicc2lem3  25436  ovolicc2lem5  25438  dyadmbl  25517  i1ff  25593  i1frn  25594  i1fima2  25596  itg2monolem1  25667  dvnres  25849  c1liplem1  25917  c1lip2  25919  dvge0  25927  lhop1lem  25934  itgsubstlem  25971  fta1glem2  26090  fta1b  26093  idomrootle  26094  plyf  26119  plypf1  26133  plyadd  26138  plymul  26139  coeeu  26146  dgrlem  26150  coeid  26159  elqaalem3  26245  aareccl  26250  eff1olem  26473  relogf1o  26491  logdmn0  26565  logcnlem2  26568  logcnlem3  26569  efopnlem1  26581  efopnlem2  26582  logtayl2  26587  cxpcn3lem  26673  cxpcn3  26674  logbgcd1irr  26720  atandmneg  26832  atandmcj  26835  efiatan2  26843  cosatan  26847  cosatanne0  26848  dvatan  26861  areage0  26889  cxp2lim  26903  jensenlem2  26914  jensen  26915  eldmgm  26948  dmgmaddn0  26949  dmlogdmgm  26950  lgamgulmlem2  26956  lgamgulmlem3  26957  lgamgulmlem5  26959  lgambdd  26963  lgamucov  26964  ftalem3  27001  efnnfsumcl  27029  efchtdvds  27085  sqff1o  27108  fsumdvdsdiaglem  27109  dvdsppwf1o  27112  dvdsflf1o  27113  musum  27117  muinv  27119  mpodvdsmulf1o  27120  dvdsmulf1o  27122  lgsfle1  27233  lgsle1  27239  lgsdirprm  27258  lgsne0  27262  lgseisenlem3  27304  lgseisenlem4  27305  lgsquadlem1  27307  lgsquadlem2  27308  chebbnd1  27399  chtppilim  27402  chpchtlim  27406  chpo1ub  27407  dchrmusumlema  27420  dchrvmasumlem1  27422  dchrisum0lema  27441  dchrisum0lem2a  27444  logsqvma  27469  selberg3lem2  27485  pntrsumo1  27492  pnt2  27540  ostthlem1  27554  ostth3  27565  sltval2  27584  leftlt  27795  rightgt  27796  precsexlem8  28139  precsexlem9  28140  precsexlem11  28142  elons2  28182  onsleft  28184  sltonold  28185  onscutleft  28187  onscutlt  28188  axtgcgrrflx  28425  axtgcgrid  28426  axtgsegcon  28427  axtg5seg  28428  axtgbtwnid  28429  axtgpasch  28430  axtgcont1  28431  tglng  28509  axcontlem7  28933  axcontlem10  28936  upgrle  29053  umgredg2  29063  lfgredgge2  29087  usgredg2ALT  29156  usgr1vr  29218  usgrexmpledg  29225  upgrres1  29276  fusgrvtxfi  29282  vtxnbuvtx  29354  cusgrcplgr  29383  vdumgr0  29444  vtxdgoddnumeven  29517  trlres  29662  usgr2pth  29727  cyclispthon  29767  clwwlknlen  29994  clwwnonrepclwwnon  30307  2clwwlk2  30310  ablocom  30510  phpar2  30785  cbncms  30827  hlph  30851  hcaucvg  31148  hlimconvi  31153  shaddcl  31179  shmulcl  31180  chlimi  31196  chcompl  31204  choc1  31289  nmopre  31832  cnopc  31875  lnopl  31876  unop  31877  hmop  31884  cnfnc  31892  lnfnl  31893  nlelshi  32022  cnlnadjlem5  32033  elpjidm  32146  mdslle1i  32279  mdslle2i  32280  atcv0  32304  chpssati  32325  aciunf1lem  32619  padct  32676  ssnnssfz  32743  ccatf1  32903  swrdrndisj  32912  ressprs  32921  pwrssmgc  32955  wrdpmtrlast  33048  cyc3evpm  33105  cycpmgcl  33108  cycpmconjslem2  33110  cyc3conja  33112  isarchi3  33139  archirng  33140  archirngz  33141  archiabllem1a  33143  archiabllem1b  33144  archiabllem2a  33146  archiabllem2c  33147  archiabllem2b  33148  archiabl  33150  isarchiofld  33151  elrgspnlem1  33192  elrgspnlem2  33193  elrgspnlem4  33195  elrgspnsubrun  33199  isdrng4  33244  nn0omnd  33292  quslsm  33352  nsgmgclem  33358  nsgmgc  33359  prmidl0  33397  qsidomlem1  33399  mxidlirred  33419  krull  33426  ufdprmidl  33488  1arithufdlem4  33494  sradrng  33554  extdg1id  33637  ply1annnr  33669  madjusmdetlem4  33796  qtophaus  33802  crefi  33813  cmpcref  33816  cmppcmp  33824  pcmplfin  33826  zart0  33845  tpr2rico  33878  rge0scvg  33915  zrhunitpreima  33942  qqhrhm  33955  esummono  34020  gsumesum  34025  esumrnmpt2  34034  esumpinfval  34039  esumpcvgval  34044  esumpmono  34045  0elsiga  34080  sigaclcu  34083  issgon  34089  inelpisys  34120  ldsysgenld  34126  ldgenpisyslem1  34129  sxuni  34159  isrnmeas  34166  measvuni  34180  measssd  34181  ddemeas  34202  imambfm  34229  elmbfmvol2  34234  dya2icoseg2  34245  omssubaddlem  34266  omssubadd  34267  carsgsigalem  34282  pmeasmono  34291  sibfinima  34306  oddpwdc  34321  oddpwdcv  34322  eulerpartlemf  34337  eulerpartlemt  34338  eulerpartlemr  34341  eulerpartlemgvv  34343  eulerpartlemgs2  34347  fiblem  34365  probtot  34379  ballotlem4  34466  ballotlem5  34467  ballotlemfrc  34494  ballotlemirc  34499  ballotth  34505  hgt750lemb  34623  bnj642  34714  bnj643  34715  bnj645  34716  bnj707  34721  bnj1379  34796  bnj1538  34821  bnj110  34824  bnj93  34829  bnj906  34896  bnj1006  34926  bnj1110  34948  bnj1121  34951  bnj1204  34978  bnj1321  34993  bnj1364  34994  bnj1398  35000  bnj1450  35016  bnj1312  35024  bnj1501  35033  bnj1523  35037  tz9.1regs  35066  0nn0m1nnn0  35085  subfacp1lem3  35154  subfacp1lem5  35156  pconncn  35196  connpconn  35207  cvmcov  35235  cvmliftlem1  35257  cvmliftlem10  35266  cvmlift2lem11  35285  cvmlift2lem12  35286  msubff1  35528  mvhf1  35531  mthmpps  35554  mclspps  35556  fundmpss  35739  funpartfun  35916  fnetg  36318  neibastop1  36332  filnetlem3  36353  onint1  36422  weiunlem2  36436  weiunpo  36438  weiunse  36441  bj-nnfa  36701  bj-idres  37133  bj-rvecrr  37270  icorempo  37324  pibt2  37390  wl-nfeqfb  37509  phpreu  37583  fin2solem  37585  fin2so  37586  lindsenlbs  37594  matunitlindflem1  37595  matunitlindflem2  37596  matunitlindf  37597  ptrest  37598  poimirlem1  37600  poimirlem2  37601  poimirlem3  37602  poimirlem4  37603  poimirlem5  37604  poimirlem6  37605  poimirlem7  37606  poimirlem8  37607  poimirlem9  37608  poimirlem10  37609  poimirlem11  37610  poimirlem12  37611  poimirlem13  37612  poimirlem14  37613  poimirlem15  37614  poimirlem16  37615  poimirlem17  37616  poimirlem18  37617  poimirlem19  37618  poimirlem20  37619  poimirlem21  37620  poimirlem22  37621  poimirlem23  37622  poimirlem24  37623  poimirlem26  37625  poimirlem27  37626  poimirlem29  37628  poimirlem31  37630  mblfinlem2  37637  dvtan  37649  itg2gt0cn  37654  ftc1anclem7  37678  ftc1anclem8  37679  ftc1anc  37680  cover2  37694  indexa  37712  istotbnd3  37750  sstotbnd2  37753  sstotbnd  37754  totbndss  37756  equivtotbnd  37757  isbnd3  37763  totbndbnd  37768  equivbnd  37769  prdsbnd  37772  prdstotbnd  37773  heibor  37800  zrdivrng  37932  crngocom  37980  isfld2  37984  dmncrng  38035  eqvrelrel  38573  disjrel  38707  disjdmqscossss  38780  prter2  38859  toycom  38951  lsateln0  38973  lpssat  38991  lssat  38994  oposlem  39160  olop  39192  omllaw  39221  cvlexch1  39306  dihpN  41315  mapdordlem2  41616  linvh  42069  idomnnzpownz  42105  idomnnzgmulnz  42106  aks6d1c5lem2  42111  deg1pow  42114  redvmptabs  42333  readvrec2  42334  readvrec  42335  mhphflem  42569  prjspertr  42578  nacsfg  42678  nacsfix  42685  mzpindd  42719  diophrw  42732  diophrex  42748  rexzrexnn0  42777  pell1234qrdich  42834  rmspecnonsq  42880  rmspecfund  42882  rmspecpos  42889  monotoddzzfi  42915  ltrmxnn0  42922  rmxnn  42924  jm2.23  42969  jm3.1lem2  42991  dnnumch3  43020  lnmlssfg  43053  lnmlmic  43061  lnrlnm  43086  lnr2i  43089  lpirlnr  43090  hbtlem6  43102  hbt  43103  mnccoe  43111  proot1mul  43167  proot1hash  43168  deg1mhm  43173  ondif1i  43235  limnsuc  43238  cantnfresb  43297  succlg  43301  ntrneifv2  44053  grucollcld  44233  mnurndlem1  44254  ismnushort  44274  radcnvrat  44287  binomcxplemdvbinom  44326  binomcxplemcvg  44327  binomcxplemnotnn0  44329  ordelordALT  44511  2uasbanh  44535  ordelordALTVD  44840  relprel  44925  elixpconstg  45067  rabidim2  45080  disjinfi  45170  supminfxr2  45449  sumnnodd  45612  stoweidlem7  45989  stoweidlem14  45996  stoweidlem16  45998  stoweidlem24  46006  stoweidlem31  46013  stoweidlem54  46036  wallispilem3  46049  fourierdlem42  46131  fourierdlem48  46136  fourierdlem51  46139  fourierdlem64  46152  fourierdlem76  46164  fourierdlem79  46167  fourierdlem81  46169  fourierdlem87  46175  etransclem28  46244  etransclem32  46248  sge0fodjrnlem  46398  hoidmvlelem3  46579  ovolval5lem3  46636  pimrecltpos  46690  pimrecltneg  46706  issmflem  46709  smfaddlem1  46745  smfsuplem1  46793  smfsuplem3  46795  smflimsuplem7  46808  smfliminflem  46812  tworepnotupword  46868  nfunsnafv  47127  faovcl  47185  tz6.12-2-afv2  47222  tz6.12i-afv2  47228  sprel  47469  evendiv2z  47617  oddp1div2z  47618  2dvdseven  47638  2ndvdsodd  47640  perfectALTVlem1  47706  sbgoldbm  47769  upgrimtrls  47890  upgrimpthslem1  47891  upgrimspths  47894  upgrimcycls  47895  uhgrimisgrgric  47915  gpgprismgr4cycllem2  48070  clintopcllaw  48183  uzlidlring  48207  rngccatidALTV  48244  funcringcsetcALTV2lem7  48268  ringccatidALTV  48278  ringcinvALTV  48282  funcringcsetclem7ALTV  48291  fldhmsubcALTV  48305  ssnn0ssfz  48321  el0ldepsnzr  48440  regt1loggt0  48509  elbigodm  48528  fllogbd  48533  rrx2xpref1o  48691  unilbss  48790  fdomne0  48822  f002  48826  xpco2  48829  imaf1homlem  49080  idemb  49132  uobeq2  49374  thincmo2  49399  thincmoALT  49402  fullthinc  49423  idfudiag1  49498  elsetrecslem  49672