Theorem simprbi 479

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  xornan  1464  sb1  1870  eumo  2487  reurmo  3138  pssne  3665  pssn2lp  3670  ssnpss  3672  eldifn  3695  elinel2  3762  rabsnt  4210  eldifsni  4261  unimax  4409  ssintub  4430  moop2  4891  pwssun  4944  weso  5029  opelxp2  5075  wfisg  5632  ordwe  5653  funmo  5820  funopg  5836  funun  5846  fununi  5878  funimaexg  5889  fndm  5904  frn  5966  f1ss  6019  f1ssr  6020  f1ssres  6021  forn  6031  f1f1orn  6061  f1orescnv  6065  f1imacnv  6066  funcocnv2  6074  dffv2  6181  exfo  6285  foelrn  6286  isorel  6476  isoini2  6489  f1ofveu  6544  fovcl  6663  f1opw  6787  onminesb  6890  onminsb  6891  tfis  6946  limomss  6962  nnlim  6970  ssnlim  6975  curry1  7156  curry2  7159  f1o2ndf1  7172  fnwelem  7179  ressuppss  7201  mpt2xopn0yelv  7226  wfrlem5  7306  tz7.48lem  7423  dif20el  7472  oeordi  7554  oeeulem  7568  oeeui  7569  nnawordex  7604  swoer  7659  erdisj  7681  eceqoveq  7740  mapsnconst  7789  ixpn0  7826  resixpfo  7832  boxcutc  7837  sdomnen  7870  en0  7905  en1  7909  domunsncan  7945  fodomr  7996  phplem4  8027  php3  8031  unxpdomlem3  8051  fineqvlem  8059  f1opwfi  8153  fsuppcolem  8189  fsuppco  8190  mapfienlem1  8193  mapfienlem2  8194  supub  8248  suplub  8249  ordtypelem2  8307  ordtypelem3  8308  ordtypelem6  8311  ordtypelem7  8312  wemapso2lem  8340  wdom2d  8368  brwdom3  8370  ixpiunwdom  8379  inf3lem2  8409  inf3lem6  8413  oancom  8431  infdifsn  8437  cantnfp1lem3  8460  cantnflem3  8471  cantnflem4  8472  oef1o  8478  cnfcom3  8484  tctr  8499  tz9.12lem3  8535  scottex  8631  cardid2  8662  infxpenlem  8719  acni3  8753  cardaleph  8795  iscard3  8799  dfac5lem4  8832  dfac5lem5  8833  kmlem1  8855  cofsmo  8974  fin4en1  9014  enfin2i  9026  fin23lem28  9045  fin23lem38  9054  isf32lem6  9063  enfin1ai  9089  isfin1-3  9091  hsmexlem2  9132  hsmexlem4  9134  domtriomlem  9147  axdc2lem  9153  axdc3lem2  9156  ac6num  9184  zorn2lem2  9202  brdom3  9231  alephval2  9273  alephreg  9283  pwcfsdom  9284  smobeth  9287  fpwwe2lem6  9336  fpwwe2lem13  9343  canthp1lem2  9354  pwfseqlem3  9361  hargch  9374  winalim2  9397  gchina  9400  inar1  9476  0npi  9583  mulclpi  9594  mulcanpi  9601  nlt1pi  9607  nqereu  9630  prcdnq  9694  prnmax  9696  ltresr2  9841  axrnegex  9862  axpre-sup  9869  eluz2gt1  11636  1nuz2  11640  zsupss  11653  rpgt0  11720  ixxss1  12064  ixxss2  12065  ixxss12  12066  lbioo  12077  ubioo  12078  iccss2  12115  iccssico2  12118  elfzuz3  12210  uzdisj  12282  nn0disj  12324  serge0  12717  expge0  12758  expge1  12759  expaddzlem  12765  hashrabsn1  13024  hashfun  13084  cshinj  13408  relexpuzrel  13640  shftfn  13661  sqrlem6  13836  rlimss  14081  lo1dm  14098  o1dm  14109  rlimrege0  14158  fsumf1o  14301  fsumge0  14368  incexc2  14409  supcvg  14427  fprodf1o  14515  divalglem9  14962  bitsfzolem  14994  bitsinv2  15003  bitsf1ocnv  15004  bitsf1  15006  gcdcllem1  15059  bezout  15098  prmind2  15236  nprm  15239  sqnprm  15252  dvdsprm  15253  isprm5  15257  coprm  15261  phibndlem  15313  dfphi2  15317  phimullem  15322  phisum  15333  pclem  15381  pcpre1  15385  pcidlem  15414  expnprm  15444  prmreclem1  15458  prmreclem2  15459  prmreclem5  15462  1arith  15469  4sqlem18  15504  vdwnnlem3  15539  ramtlecl  15542  rami  15557  0ram  15562  ramub1lem1  15568  prmgaplem5  15597  firest  15916  acsfiel  16138  isacs1i  16141  catlid  16167  catrid  16168  fullfo  16395  fthf1  16400  fthoppc  16406  invfuc  16457  prslem  16754  posi  16773  dlatmjdi  17017  pslem  17029  tsrlin  17042  cnvtsr  17045  tsrdir  17061  mndid  17126  mhmf  17163  mhmlin  17165  mhm0  17166  mrcmndind  17189  grpinvex  17255  grplinv  17291  mulgz  17391  mulgdirlem  17395  mulgdir  17396  mulgass  17402  nsgbi  17448  nmzbi  17457  ghmf  17487  ghmlin  17488  conjnsg  17519  gimf1o  17528  gagrpid  17550  gaf  17551  gaass  17553  psgnunilem5  17737  odid  17780  odf1o2  17811  gexid  17819  sylow1lem4  17839  odcau  17842  pj1id  17935  efgredeu  17988  ablcmn  18022  cmncom  18032  mulgdi  18055  gexexlem  18078  torsubg  18080  cyggenod2  18110  cygctb  18116  ghmcyg  18120  dprdf1o  18254  dprd2dlem1  18263  dprd2da  18264  ablfacrplem  18287  ablfaclem2  18308  ablfac2  18311  crngmgp  18378  rhmmhm  18545  rhmghm  18548  drngunit  18575  drngmgp  18582  drngid  18584  subrgss  18604  subrg1cl  18611  issubdrg  18628  abvge0  18648  srngcnv  18676  lmhmlin  18856  lmimf1o  18884  lvecdrng  18926  lspsolvlem  18963  islbs3  18976  lbsextlem3  18981  2idlcpbl  19055  nzrnz  19081  opprnzr  19086  rrgeq0i  19110  domneq0  19118  domnrrg  19121  drngdomn  19124  fldidom  19126  assalem  19137  mplsubrglem  19260  mplcoe1  19286  mplbas2  19291  opsrtoslem2  19306  mplelsfi  19312  coe1mul2  19460  zringunit  19655  prmirredlem  19660  znidomb  19729  cygzn  19738  psgndiflemB  19765  pjf  19876  frlmsslsp  19954  frlmlbs  19955  f1lindf  19980  pmatcoe1fsupp  20325  toponuni  20542  tpsuni  20553  clsval2  20664  mretopd  20706  neips  20727  neiptoptop  20745  neiptopnei  20746  perflp  20768  perfi  20769  restfpw  20793  cnf  20860  cnpf  20861  cnpimaex  20870  cnima  20879  t0sep  20938  t1sncld  20940  t1ficld  20941  hausnei  20942  regsep  20948  pnrmcld  20956  nrmsep3  20969  cnrmi  20974  cmpcov  21002  discmp  21011  tgcmp  21014  uncmp  21016  hauscmplem  21019  cmpfi  21021  conclo  21028  1stcclb  21057  2ndcdisj  21069  llyi  21087  nllyi  21088  ptpjpre1  21184  ptpjcn  21224  ptpjopn  21225  ptclsg  21228  dfac14  21231  txdis1cn  21248  pthaus  21251  hauseqlcld  21259  txkgen  21265  xkococn  21273  txcon  21302  hmeocnvcn  21374  fbssfi  21451  filss  21467  ufilss  21519  uffixfr  21537  flimneiss  21580  flimelbas  21582  fclscf  21639  flimfnfcls  21642  alexsublem  21658  alexsubb  21660  alexsubALT  21665  ptcmplem2  21667  ptcmplem3  21668  ptcmplem4  21669  tmdgsum2  21710  ghmcnp  21728  tgpt0  21732  qustgplem  21734  tsmsfbas  21741  tsmslem1  21742  tsmsgsum  21752  tsmssubm  21756  tsmsres  21757  tsmsf1o  21758  tsmsmhm  21759  tsmsadd  21760  tsmsxplem1  21766  tsmsxplem2  21767  tsmsxp  21768  istdrg2  21791  vscacn  21799  tvctdrg  21806  uspreg  21888  ucncn  21899  neipcfilu  21910  cuspcvg  21915  psmetxrge0  21928  isxmet2d  21942  prdsxmetlem  21983  imasdsf1olem  21988  xmstopn  22066  mstopn  22067  stdbdxmet  22130  prdsxmslem2  22144  nrgabv  22275  nmvs  22290  nvclvec  22311  nmoge0  22335  nghmcl  22341  nmoi  22342  nghmghm  22348  nmhmlmhm  22363  nmhmnghm  22364  icccmp  22436  xrge0gsumle  22444  xrge0tsms  22445  metds0  22461  metdstri  22462  metdsre  22464  metdseq0  22465  metdscnlem  22466  metnrmlem1a  22469  icopnfcnv  22549  xrhmeo  22553  pcoval1  22621  cvslvec  22733  cvsunit  22739  cphreccllem  22786  cmetcvg  22891  lmle  22907  cmscmet  22951  cmetcusp1  22957  hlcph  22968  minveclem4  23011  ivthlem3  23029  ovolmge0  23052  ovolicc1  23091  ovolicc2lem3  23094  ovolicc2lem5  23096  mblsplit  23107  dyadmbl  23174  mbfdm  23201  mbfadd  23234  mbfsub  23235  i1ff  23249  i1frn  23250  i1fima2  23252  mbfmul  23299  itg2monolem1  23323  bddmulibl  23411  dvnres  23500  c1liplem1  23563  c1lip2  23565  dvge0  23573  lhop1lem  23580  itgsubstlem  23615  fta1glem1  23729  fta1glem2  23730  fta1b  23733  plyf  23758  plypf1  23772  plyadd  23777  plymul  23778  coeeu  23785  dgrlem  23789  coeid  23798  elqaalem3  23880  aareccl  23885  eff1olem  24098  relogf1o  24117  logdmn0  24186  logcnlem2  24189  logcnlem3  24190  dvloglem  24194  efopnlem1  24202  efopnlem2  24203  logtayl2  24208  cxpcn3lem  24288  cxpcn3  24289  atandmneg  24433  atandmcj  24436  efiatan2  24444  cosatan  24448  cosatanne0  24449  dvatan  24462  areage0  24490  cxp2lim  24503  jensenlem2  24514  jensen  24515  eldmgm  24548  dmgmaddn0  24549  dmlogdmgm  24550  lgamgulmlem2  24556  lgamgulmlem3  24557  lgamgulmlem5  24559  lgambdd  24563  lgamucov  24564  wilthlem1  24594  wilth  24597  ftalem3  24601  efnnfsumcl  24629  isppw  24640  efchtdvds  24685  sqff1o  24708  fsumdvdsdiaglem  24709  dvdsppwf1o  24712  dvdsflf1o  24713  musum  24717  muinv  24719  dvdsmulf1o  24720  fsumvma2  24739  vmasum  24741  chpval2  24743  chpchtsum  24744  chpub  24745  mersenne  24752  perfect1  24753  bposlem1  24809  lgsfle1  24831  lgsle1  24837  lgsdirprm  24856  lgsne0  24860  lgseisenlem3  24902  lgseisenlem4  24903  lgsquadlem1  24905  lgsquadlem2  24906  2sqblem  24956  chebbnd1lem1  24958  chebbnd1  24961  chtppilim  24964  chpchtlim  24968  chpo1ub  24969  rplogsumlem2  24974  rpvmasumlem  24976  dchrmusumlema  24982  dchrvmasumlem1  24984  dchrisum0flblem2  24998  dchrisum0lema  25003  dchrisum0lem2a  25006  logsqvma  25031  selberg3lem2  25047  pntrsumo1  25054  pnt2  25102  ostthlem1  25116  ostth3  25127  axtgcgrrflx  25161  axtgcgrid  25162  axtgsegcon  25163  axtg5seg  25164  axtgbtwnid  25165  axtgpasch  25166  axtgcont1  25167  tglng  25241  axcontlem7  25650  axcontlem10  25653  upgrle  25757  umgredg2  25766  lfgredgge2  25790  umgrale  25850  usgraedg2  25904  usgraexmpledg  25932  clwlkfclwwlk1hashn  26368  eupatrl  26495  ablocom  26786  phpar2  27062  cbncms  27105  hlph  27129  hcaucvg  27427  hlimconvi  27432  shaddcl  27458  shmulcl  27459  chlimi  27475  chcompl  27483  choc1  27570  nmopre  28113  cnopc  28156  lnopl  28157  unop  28158  hmop  28165  cnfnc  28173  lnfnl  28174  nlelshi  28303  cnlnadjlem5  28314  elpjidm  28427  mdslle1i  28560  mdslle2i  28561  atcv0  28585  chpssati  28606  fovcld  28820  aciunf1lem  28844  padct  28885  ssnnssfz  28937  ressprs  28986  oduprs  28987  resspos  28990  resstos  28991  tleile  28992  ogrpinvOLD  29046  ogrpinv0le  29047  ogrpsub  29048  ogrpaddlt  29049  isarchi3  29072  archirng  29073  archirngz  29074  archiabllem1a  29076  archiabllem1b  29077  archiabllem2a  29079  archiabllem2c  29080  archiabllem2b  29081  archiabl  29083  orngsqr  29135  ornglmulle  29136  orngrmulle  29137  ofldtos  29142  ofldlt1  29144  ofldchr  29145  suborng  29146  subofld  29147  isarchiofld  29148  nn0omnd  29172  madjusmdetlem4  29224  qtophaus  29231  crefi  29242  cmpcref  29245  cmppcmp  29253  pcmplfin  29255  tpr2rico  29286  rge0scvg  29323  zrhunitpreima  29350  qqhrhm  29361  esummono  29443  gsumesum  29448  esumrnmpt2  29457  esumpinfval  29462  esumpcvgval  29467  esumpmono  29468  0elsiga  29504  sigaclcu  29507  issgon  29513  inelpisys  29544  ldsysgenld  29550  ldgenpisyslem1  29553  sxuni  29583  isrnmeas  29590  measvuni  29604  measssd  29605  ddemeas  29626  imambfm  29651  elmbfmvol2  29656  dya2icoseg2  29667  omssubaddlem  29688  omssubadd  29689  carsgsigalem  29704  pmeasmono  29713  sibfinima  29728  oddpwdc  29743  oddpwdcv  29744  eulerpartlemf  29759  eulerpartlemt  29760  eulerpartlemr  29763  eulerpartlemgvv  29765  eulerpartlemgs2  29769  sseqf  29781  fiblem  29787  probtot  29801  ballotlem4  29887  ballotlem5  29888  ballotlemfrc  29915  ballotlemirc  29920  ballotth  29926  bnj642  30072  bnj643  30073  bnj645  30074  bnj707  30079  bnj1379  30155  bnj1538  30179  bnj110  30182  bnj93  30187  bnj906  30254  bnj1006  30283  bnj1110  30304  bnj1121  30307  bnj1172  30323  bnj1204  30334  bnj1321  30349  bnj1364  30350  bnj1398  30356  bnj1450  30372  bnj1312  30380  bnj1501  30389  bnj1523  30393  subfacp1lem3  30418  subfacp1lem5  30420  pconcn  30460  sconpht  30465  conpcon  30471  cvmcov  30499  cvmliftlem1  30521  cvmliftlem10  30530  cvmlift2lem11  30549  cvmlift2lem12  30550  msubff1  30707  mvhf1  30710  mthmpps  30733  mclspps  30735  fundmpss  30910  tfisg  30960  frinsg  30986  frrlem5  31028  sltval2  31053  txpss3v  31155  pprodss4v  31161  fnetg  31510  neibastop1  31524  filnetlem3  31545  onint1  31618  bj-elid2  32263  icorempt2  32375  wl-nfeqfb  32502  phpreu  32563  fin2solem  32565  fin2so  32566  lindsenlbs  32574  matunitlindflem1  32575  matunitlindflem2  32576  matunitlindf  32577  ptrest  32578  poimirlem1  32580  poimirlem2  32581  poimirlem3  32582  poimirlem4  32583  poimirlem5  32584  poimirlem6  32585  poimirlem7  32586  poimirlem8  32587  poimirlem9  32588  poimirlem10  32589  poimirlem11  32590  poimirlem12  32591  poimirlem13  32592  poimirlem14  32593  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem18  32597  poimirlem19  32598  poimirlem20  32599  poimirlem21  32600  poimirlem22  32601  poimirlem23  32602  poimirlem24  32603  poimirlem26  32605  poimirlem27  32606  poimirlem29  32608  poimirlem31  32610  mblfinlem2  32617  dvtan  32630  itg2gt0cn  32635  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  cover2  32678  indexa  32698  istotbnd3  32740  sstotbnd2  32743  sstotbnd  32744  totbndss  32746  equivtotbnd  32747  isbnd3  32753  totbndbnd  32758  equivbnd  32759  prdsbnd  32762  prdstotbnd  32763  heibor  32790  mndoisexid  32838  zrdivrng  32922  crngocom  32970  isfld2  32974  dmncrng  33025  prter2  33184  toycom  33278  lsateln0  33300  lpssat  33318  lssat  33321  oposlem  33487  olop  33519  omllaw  33548  cvlexch1  33633  dihpN  35643  mapdordlem2  35944  nacsfg  36286  nacsfix  36293  mzpindd  36327  diophrw  36340  diophrex  36357  rexzrexnn0  36386  pell1234qrdich  36443  rmspecsqrtnqOLD  36489  rmspecnonsq  36490  rmspecfund  36492  rmspecpos  36499  monotoddzzfi  36525  ltrmxnn0  36534  rmxnn  36536  jm2.23  36581  jm3.1lem2  36603  dnnumch3  36635  lnmlssfg  36668  lnmlmic  36676  lnrlnm  36702  lnr2i  36705  lpirlnr  36706  hbtlem6  36718  hbt  36719  mnccoe  36727  cntzsdrg  36791  idomrootle  36792  proot1mul  36796  proot1hash  36797  deg1mhm  36804  ntrneifv2  37398  radcnvrat  37535  binomcxplemdvbinom  37574  binomcxplemcvg  37575  binomcxplemnotnn0  37577  ordelordALT  37768  2uasbanh  37798  ordelordALTVD  38125  elixpconstg  38294  foelrnf  38368  disjinfi  38375  sumnnodd  38697  stoweidlem7  38900  stoweidlem14  38907  stoweidlem16  38909  stoweidlem24  38917  stoweidlem31  38924  stoweidlem54  38947  wallispilem3  38960  fourierdlem42  39042  fourierdlem48  39047  fourierdlem51  39050  fourierdlem64  39063  fourierdlem76  39075  fourierdlem79  39078  fourierdlem81  39080  fourierdlem87  39086  etransclem28  39155  etransclem32  39159  sge0fodjrnlem  39309  hoidmvlelem3  39487  preimagelt  39589  preimalegt  39590  pimrecltpos  39596  pimrecltneg  39610  issmflem  39613  smfaddlem1  39649  2reu1  39835  nfunsnafv  39871  faovcl  39929  evendiv2z  40083  oddp1div2z  40084  2dvdseven  40104  2ndvdsodd  40105  perfectALTVlem1  40164  usgredg2ALT  40420  usgr1vr  40481  usgrexmpledg  40486  upgrres1  40532  fusgrvtxfi  40538  nbfusgrlevtxm1  40605  nbfusgrlevtxm2  40606  cusgrcplgr  40642  vdumgr0  40695  trlres  40908  usgr2pth  40970  umgrn1cycl  41010  clwlksfclwwlk1hashn  41266  clintopcllaw  41637  0ringbas  41661  rnghmmgmhm  41684  uzlidlring  41719  rnghmsubcsetclem1  41767  rngccatidALTV  41781  zrinitorngc  41792  zrtermorngc  41793  rhmsubcsetclem1  41813  funcringcsetcALTV2lem7  41834  ringccatidALTV  41844  funcringcsetclem7ALTV  41857  irinitoringc  41861  zrtermoringc  41862  fldhmsubc  41876  fldhmsubcALTV  41895  ssnn0ssfz  41920  el0ldepsnzr  42050  regt1loggt0  42128  elbigodm  42147  fllogbd  42152  elsetrecslem  42243