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 215	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
3	2	simprd 496	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  simplbiim  505  xornan  1515  eumo  2579  reurmo  3365  pssne  4032  pssn2lp  4037  ssnpss  4039  eldifn  4063  elinel2  4131  rabsnt  4668  eldifsni  4724  unimax  4878  ssintub  4898  moop2  5417  pwssun  5486  weso  5581  opelxp2  5632  predpo  6230  frpoinsg  6250  wfisgOLD  6261  ordwe  6283  funmo  6456  funmoOLD  6457  funopg  6475  funun  6487  fununi  6516  funimaexg  6527  fndm  6545  frn  6616  f1ss  6685  f1ssr  6686  forn  6700  f1f1orn  6736  f1orescnv  6740  f1imacnv  6741  funcocnv2  6750  dffv2  6872  exfo  6990  foelrn  6991  isorel  7206  isoini2  7219  f1ofveu  7279  fovcl  7411  onminesb  7652  onminsb  7653  tfis  7710  limomss  7726  nnlim  7735  ssnlim  7741  curry1  7953  curry2  7956  f1o2ndf1  7972  fnwelem  7981  mpoxopn0yelv  8038  wfrlem5OLD  8153  tz7.48lem  8281  dif20el  8344  oeordi  8427  oeeulem  8441  oeeui  8442  nnawordex  8477  swoer  8537  eceqoveq  8620  mapsnconst  8689  resixpfo  8733  boxcutc  8738  sdomnen  8778  en0  8812  en0OLD  8813  en0ALT  8814  en0r  8815  en1  8820  en1OLD  8821  dom0  8898  fodomr  8924  dif1enlem  8952  unxpdomlem3  9038  fineqvlem  9046  f1opwfi  9132  fsuppcolem  9169  fsuppco  9170  mapfienlem1  9173  mapfienlem2  9174  supub  9227  suplub  9228  ordtypelem2  9287  ordtypelem3  9288  ordtypelem6  9291  ordtypelem7  9292  wemapso2lem  9320  wdom2d  9348  brwdom3  9350  ixpiunwdom  9358  inf3lem2  9396  inf3lem6  9400  oancom  9418  infdifsn  9424  cantnfp1lem3  9447  cantnflem3  9458  cantnflem4  9459  oef1o  9465  cnfcom3  9471  tctr  9507  frinsg  9518  tz9.12lem3  9556  scottex  9652  cardid2  9720  infxpenlem  9778  acni3  9812  cardaleph  9854  iscard3  9858  dfac5lem4  9891  dfac5lem5  9892  kmlem1  9915  cofsmo  10034  fin4en1  10074  enfin2i  10086  fin23lem28  10105  fin23lem38  10114  isf32lem6  10123  enfin1ai  10149  hsmexlem2  10192  hsmexlem4  10194  domtriomlem  10207  axdc2lem  10213  axdc3lem2  10216  ac6num  10244  zorn2lem2  10262  brdom3  10293  alephval2  10337  alephreg  10347  pwcfsdom  10348  smobeth  10351  fpwwe2lem5  10400  fpwwe2lem12  10407  canthp1lem2  10418  pwfseqlem3  10425  hargch  10438  winalim2  10461  gchina  10464  inar1  10540  0npi  10647  mulclpi  10658  mulcanpi  10665  nlt1pi  10671  nqereu  10694  prcdnq  10758  prnmax  10760  ltresr2  10906  axrnegex  10927  axpre-sup  10934  eluz2gt1  12669  1nuz2  12673  zsupss  12686  rpgt0  12751  ixxss1  13106  ixxss2  13107  ixxss12  13108  lbioo  13119  ubioo  13120  iccss2  13159  iccssico2  13162  elfzuz3  13262  serge0  13786  expge0  13828  expge1  13829  expaddzlem  13835  hashrabsn1  14098  hashfun  14161  cshinj  14533  relexpuzrel  14772  shftfn  14793  sqrlem6  14968  rlimss  15220  lo1dm  15237  o1dm  15248  rlimrege0  15297  fsumf1o  15444  fsumge0  15516  incexc2  15559  supcvg  15577  fprodf1o  15665  divalglem9  16119  bitsfzolem  16150  bitsf1  16162  gcdcllem1  16215  bezout  16260  nprm  16402  dvdsprm  16417  coprm  16425  dfphi2  16484  phimullem  16489  phisum  16500  expnprm  16612  prmreclem2  16627  prmreclem5  16630  1arith  16637  4sqlem18  16672  vdwnnlem3  16707  ramtlecl  16710  rami  16725  0ram  16730  ramub1lem1  16736  prmgaplem5  16765  acsfiel  17372  isacs1i  17375  catlid  17401  catrid  17402  fullfo  17637  fthf1  17642  fthoppc  17648  invfuc  17701  prslem  18025  posi  18044  tleile  18148  dlatmjdi  18250  pslem  18299  tsrlin  18312  cnvtsr  18315  tsrdir  18331  mndid  18404  mhmf  18444  mhmlin  18446  mhm0  18447  mndind  18475  grpinvex  18596  grplinv  18637  mulgz  18740  mulgdirlem  18743  mulgdir  18744  mulgass  18749  nsgbi  18794  nmzbi  18801  ghmf  18847  ghmlin  18848  conjnsg  18879  gimf1o  18888  gagrpid  18909  gaf  18910  gaass  18912  psgnunilem5  19111  odid  19155  odf1o2  19187  gexid  19195  sylow1lem4  19215  pj1id  19314  efgredeu  19367  ablcmn  19402  cmncom  19412  mulgdi  19437  torsubg  19464  cyggenod2  19494  cygctb  19502  ghmcyg  19506  dprdf1o  19644  ablfacrplem  19677  ablfaclem2  19698  ablfac2  19701  simpg2nsg  19708  fincygsubgodexd  19725  crngmgp  19800  rhmmhm  19975  rhmghm  19978  drngunit  20005  drngmgp  20012  drngid  20014  subrgss  20034  subrg1cl  20041  issubdrg  20058  cntzsdrg  20079  abvge0  20094  srngcnv  20122  lmhmlin  20306  lmimf1o  20334  lvecdrng  20376  lspsolvlem  20413  islbs3  20426  lbsextlem3  20431  2idlcpbl  20514  nzrnz  20540  opprnzr  20545  rrgeq0i  20569  domneq0  20577  domnrrg  20580  drngdomn  20583  fldidomOLD  20586  zringunit  20697  prmirredlem  20703  znidomb  20778  cygzn  20787  psgndiflemB  20814  pjf  20929  frlmsslsp  21012  frlmlbs  21013  f1lindf  21038  assalem  21073  psrbaglefi  21144  mplelsfi  21210  mplsubrglem  21219  mplcoe1  21247  mplbas2  21252  opsrtoslem2  21272  mhpmulcl  21348  coe1mul2  21449  pmatcoe1fsupp  21859  toponuni  22072  tpsuni  22094  mretopd  22252  neips  22273  neiptoptop  22291  neiptopnei  22292  perflp  22314  perfi  22315  cnf  22406  cnpf  22407  cnpimaex  22416  cnima  22425  t0sep  22484  t1ficld  22487  hausnei  22488  pnrmcld  22502  cnrmi  22520  cmpcov  22549  tgcmp  22561  hauscmplem  22566  connclo  22575  1stcclb  22604  2ndcdisj  22616  llyi  22634  nllyi  22635  ptpjpre1  22731  ptpjcn  22771  ptpjopn  22772  ptclsg  22775  dfac14  22778  txdis1cn  22795  pthaus  22798  hauseqlcld  22806  txkgen  22812  xkococn  22820  txconn  22849  hmeocnvcn  22921  fbssfi  22997  filss  23013  uffixfr  23083  flimneiss  23126  flimelbas  23128  flimfnfcls  23188  alexsubb  23206  alexsubALT  23211  ptcmplem2  23213  ptcmplem3  23214  ptcmplem4  23215  tmdgsum2  23256  ghmcnp  23275  tgpt0  23279  qustgplem  23281  istdrg2  23338  vscacn  23346  tvctdrg  23353  uspreg  23435  ucncn  23446  neipcfilu  23457  cuspcvg  23462  psmetxrge0  23475  isxmet2d  23489  prdsxmetlem  23530  imasdsf1olem  23535  xmstopn  23613  mstopn  23614  stdbdxmet  23680  prdsxmslem2  23694  nrgabv  23834  nmvs  23849  nvclvec  23870  nmoge0  23894  nghmcl  23900  nmoi  23901  nghmghm  23907  nmhmlmhm  23922  nmhmnghm  23923  icccmp  23997  xrge0gsumle  24005  metds0  24022  metdstri  24023  metdsre  24025  metdseq0  24026  metdscnlem  24027  metnrmlem1a  24030  icopnfcnv  24114  xrhmeo  24118  pcoval1  24185  cvslvec  24297  cvsunit  24303  recvs  24318  cphreccllem  24351  cphsscph  24424  cmetcvg  24458  lmle  24474  cmscmet  24519  cmetcusp1  24526  hlcph  24537  minveclem4  24605  ivthlem3  24626  ovolmge0  24650  ovolicc1  24689  ovolicc2lem3  24692  ovolicc2lem5  24694  dyadmbl  24773  i1ff  24849  i1frn  24850  i1fima2  24852  itg2monolem1  24924  dvnres  25104  c1liplem1  25169  c1lip2  25171  dvge0  25179  lhop1lem  25186  itgsubstlem  25221  fta1glem2  25340  fta1b  25343  plyf  25368  plypf1  25382  plyadd  25387  plymul  25388  coeeu  25395  dgrlem  25399  coeid  25408  elqaalem3  25490  aareccl  25495  eff1olem  25713  relogf1o  25731  logdmn0  25804  logcnlem2  25807  logcnlem3  25808  efopnlem1  25820  efopnlem2  25821  logtayl2  25826  cxpcn3lem  25909  cxpcn3  25910  logbgcd1irr  25953  atandmneg  26065  atandmcj  26068  efiatan2  26076  cosatan  26080  cosatanne0  26081  dvatan  26094  areage0  26122  cxp2lim  26135  jensenlem2  26146  jensen  26147  eldmgm  26180  dmgmaddn0  26181  dmlogdmgm  26182  lgamgulmlem2  26188  lgamgulmlem3  26189  lgamgulmlem5  26191  lgambdd  26195  lgamucov  26196  ftalem3  26233  efnnfsumcl  26261  efchtdvds  26317  sqff1o  26340  fsumdvdsdiaglem  26341  dvdsppwf1o  26344  dvdsflf1o  26345  musum  26349  muinv  26351  dvdsmulf1o  26352  lgsfle1  26463  lgsle1  26469  lgsdirprm  26488  lgsne0  26492  lgseisenlem3  26534  lgseisenlem4  26535  lgsquadlem1  26537  lgsquadlem2  26538  chebbnd1  26629  chtppilim  26632  chpchtlim  26636  chpo1ub  26637  dchrmusumlema  26650  dchrvmasumlem1  26652  dchrisum0lema  26671  dchrisum0lem2a  26674  logsqvma  26699  selberg3lem2  26715  pntrsumo1  26722  pnt2  26770  ostthlem1  26784  ostth3  26795  axtgcgrrflx  26832  axtgcgrid  26833  axtgsegcon  26834  axtg5seg  26835  axtgbtwnid  26836  axtgpasch  26837  axtgcont1  26838  tglng  26916  axcontlem7  27347  axcontlem10  27350  upgrle  27469  umgredg2  27479  lfgredgge2  27503  usgredg2ALT  27569  usgr1vr  27631  usgrexmpledg  27638  upgrres1  27689  fusgrvtxfi  27695  vtxnbuvtx  27767  cusgrcplgr  27796  vdumgr0  27856  vtxdgoddnumeven  27929  trlres  28077  usgr2pth  28141  cyclispthon  28178  clwwlknlen  28405  clwwnonrepclwwnon  28718  2clwwlk2  28721  ablocom  28919  phpar2  29194  cbncms  29236  hlph  29260  hcaucvg  29557  hlimconvi  29562  shaddcl  29588  shmulcl  29589  chlimi  29605  chcompl  29613  choc1  29698  nmopre  30241  cnopc  30284  lnopl  30285  unop  30286  hmop  30293  cnfnc  30301  lnfnl  30302  nlelshi  30431  cnlnadjlem5  30442  elpjidm  30555  mdslle1i  30688  mdslle2i  30689  atcv0  30713  chpssati  30734  fovcld  30984  aciunf1lem  31008  padct  31063  ssnnssfz  31117  ccatf1  31232  swrdrndisj  31238  ressprs  31250  oduprs  31251  resspos  31253  resstos  31254  pwrssmgc  31287  ogrpinv0le  31350  ogrpsub  31351  ogrpaddlt  31352  cyc3evpm  31426  cycpmgcl  31429  cycpmconjslem2  31431  cyc3conja  31433  isarchi3  31450  archirng  31451  archirngz  31452  archiabllem1a  31454  archiabllem1b  31455  archiabllem2a  31457  archiabllem2c  31458  archiabllem2b  31459  archiabl  31461  orngsqr  31512  ornglmulle  31513  orngrmulle  31514  ofldtos  31519  ofldlt1  31521  ofldchr  31522  suborng  31523  subofld  31524  isarchiofld  31525  nn0omnd  31554  quslsm  31602  nsgmgclem  31605  nsgmgc  31606  prmidl0  31635  qsidomlem1  31637  krull  31652  sradrng  31682  extdg1id  31747  madjusmdetlem4  31789  qtophaus  31795  crefi  31806  cmpcref  31809  cmppcmp  31817  pcmplfin  31819  zart0  31838  tpr2rico  31871  rge0scvg  31908  zrhunitpreima  31937  qqhrhm  31948  esummono  32031  gsumesum  32036  esumrnmpt2  32045  esumpinfval  32050  esumpcvgval  32055  esumpmono  32056  0elsiga  32091  sigaclcu  32094  issgon  32100  inelpisys  32131  ldsysgenld  32137  ldgenpisyslem1  32140  sxuni  32170  isrnmeas  32177  measvuni  32191  measssd  32192  ddemeas  32213  imambfm  32238  elmbfmvol2  32243  dya2icoseg2  32254  omssubaddlem  32275  omssubadd  32276  carsgsigalem  32291  pmeasmono  32300  sibfinima  32315  oddpwdc  32330  oddpwdcv  32331  eulerpartlemf  32346  eulerpartlemt  32347  eulerpartlemr  32350  eulerpartlemgvv  32352  eulerpartlemgs2  32356  fiblem  32374  probtot  32388  ballotlem4  32474  ballotlem5  32475  ballotlemfrc  32502  ballotlemirc  32507  ballotth  32513  hgt750lemb  32645  bnj642  32737  bnj643  32738  bnj645  32739  bnj707  32744  bnj1379  32819  bnj1538  32844  bnj110  32847  bnj93  32852  bnj906  32919  bnj1006  32949  bnj1110  32971  bnj1121  32974  bnj1204  33001  bnj1321  33016  bnj1364  33017  bnj1398  33023  bnj1450  33039  bnj1312  33047  bnj1501  33056  bnj1523  33060  0nn0m1nnn0  33080  subfacp1lem3  33153  subfacp1lem5  33155  pconncn  33195  connpconn  33206  cvmcov  33234  cvmliftlem1  33256  cvmliftlem10  33265  cvmlift2lem11  33284  cvmlift2lem12  33285  msubff1  33527  mvhf1  33530  mthmpps  33553  mclspps  33555  fundmpss  33749  tfisg  33795  sltval2  33868  funpartfun  34254  fnetg  34543  neibastop1  34557  filnetlem3  34578  onint1  34647  bj-nnfa  34919  bj-idres  35340  bj-rvecrr  35477  icorempo  35531  pibt2  35597  wl-nfeqfb  35704  phpreu  35770  fin2solem  35772  fin2so  35773  lindsenlbs  35781  matunitlindflem1  35782  matunitlindflem2  35783  matunitlindf  35784  ptrest  35785  poimirlem1  35787  poimirlem2  35788  poimirlem3  35789  poimirlem4  35790  poimirlem5  35791  poimirlem6  35792  poimirlem7  35793  poimirlem8  35794  poimirlem9  35795  poimirlem10  35796  poimirlem11  35797  poimirlem12  35798  poimirlem13  35799  poimirlem14  35800  poimirlem15  35801  poimirlem16  35802  poimirlem17  35803  poimirlem18  35804  poimirlem19  35805  poimirlem20  35806  poimirlem21  35807  poimirlem22  35808  poimirlem23  35809  poimirlem24  35810  poimirlem26  35812  poimirlem27  35813  poimirlem29  35815  poimirlem31  35817  mblfinlem2  35824  dvtan  35836  itg2gt0cn  35841  ftc1anclem7  35865  ftc1anclem8  35866  ftc1anc  35867  cover2  35881  indexa  35900  istotbnd3  35938  sstotbnd2  35941  sstotbnd  35942  totbndss  35944  equivtotbnd  35945  isbnd3  35951  totbndbnd  35956  equivbnd  35957  prdsbnd  35960  prdstotbnd  35961  heibor  35988  zrdivrng  36120  crngocom  36168  isfld2  36172  dmncrng  36223  eqvrelrel  36717  disjrel  36848  prter2  36902  toycom  36994  lsateln0  37016  lpssat  37034  lssat  37037  oposlem  37203  olop  37235  omllaw  37264  cvlexch1  37349  dihpN  39357  mapdordlem2  39658  fldcrngd  40262  mhphflem  40291  prjspertr  40451  nacsfg  40534  nacsfix  40541  mzpindd  40575  diophrw  40588  diophrex  40604  rexzrexnn0  40633  pell1234qrdich  40690  rmspecnonsq  40736  rmspecfund  40738  rmspecpos  40745  monotoddzzfi  40771  ltrmxnn0  40778  rmxnn  40780  jm2.23  40825  jm3.1lem2  40847  dnnumch3  40879  lnmlssfg  40912  lnmlmic  40920  lnrlnm  40945  lnr2i  40948  lpirlnr  40949  hbtlem6  40961  hbt  40962  mnccoe  40970  idomrootle  41027  proot1mul  41031  proot1hash  41032  deg1mhm  41039  ntrneifv2  41697  grucollcld  41885  mnurndlem1  41906  ismnushort  41926  radcnvrat  41939  binomcxplemdvbinom  41978  binomcxplemcvg  41979  binomcxplemnotnn0  41981  ordelordALT  42164  2uasbanh  42188  ordelordALTVD  42494  elixpconstg  42646  rabidim2  42659  foelrnf  42731  disjinfi  42738  supminfxr2  43016  sumnnodd  43178  stoweidlem7  43555  stoweidlem14  43562  stoweidlem16  43564  stoweidlem24  43572  stoweidlem31  43579  stoweidlem54  43602  wallispilem3  43615  fourierdlem42  43697  fourierdlem48  43702  fourierdlem51  43705  fourierdlem64  43718  fourierdlem76  43730  fourierdlem79  43733  fourierdlem81  43735  fourierdlem87  43741  etransclem28  43810  etransclem32  43814  sge0fodjrnlem  43961  hoidmvlelem3  44142  pimrecltpos  44253  pimrecltneg  44269  issmflem  44272  smfaddlem1  44308  smfsuplem1  44355  smfsuplem3  44357  smflimsuplem7  44370  smfliminflem  44374  nfunsnafv  44645  faovcl  44703  tz6.12-2-afv2  44740  tz6.12i-afv2  44746  sprel  44947  evendiv2z  45095  oddp1div2z  45096  2dvdseven  45116  2ndvdsodd  45118  perfectALTVlem1  45184  sbgoldbm  45247  clintopcllaw  45416  0ringbas  45440  rnghmmgmhm  45463  uzlidlring  45498  rnghmsubcsetclem1  45544  rngccatidALTV  45558  zrinitorngc  45569  zrtermorngc  45570  rhmsubcsetclem1  45590  funcringcsetcALTV2lem7  45611  ringccatidALTV  45621  funcringcsetclem7ALTV  45634  irinitoringc  45638  zrtermoringc  45639  fldhmsubc  45653  fldhmsubcALTV  45671  ssnn0ssfz  45696  el0ldepsnzr  45819  regt1loggt0  45893  elbigodm  45912  fllogbd  45917  rrx2xpref1o  46075  unilbss  46174  fdomne0  46188  f002  46192  thincmo2  46320  thincmoALT  46322  fullthinc  46338  elsetrecslem  46415  tworepnotupword  46532