Theorem simprbi 489

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  simplbiim  497  xornan  1497  sb1ALT  2510  eumo  2598  reurmo  3366  pssne  3956  pssn2lp  3961  ssnpss  3963  eldifn  3987  elinel2  4055  rabsnt  4537  eldifsni  4592  unimax  4743  ssintub  4763  moop2  5244  pwssun  5304  weso  5394  opelxp2  5445  wfisg  6018  ordwe  6039  funmo  6201  funopg  6219  funun  6230  fununi  6259  fndm  6285  frn  6347  f1ss  6406  f1ssr  6407  forn  6419  f1f1orn  6452  f1orescnv  6456  f1imacnv  6457  funcocnv2  6465  dffv2  6582  exfo  6692  foelrn  6693  isorel  6900  isoini2  6913  f1ofveu  6969  fovcl  7093  onminesb  7327  onminsb  7328  tfis  7383  limomss  7399  nnlim  7407  ssnlim  7412  curry1  7605  curry2  7608  f1o2ndf1  7621  fnwelem  7628  mpoxopn0yelv  7680  wfrlem5  7761  tz7.48lem  7878  dif20el  7930  oeordi  8012  oeeulem  8026  oeeui  8027  nnawordex  8062  swoer  8117  eceqoveq  8200  mapsnconst  8252  resixpfo  8295  boxcutc  8300  sdomnen  8333  en0  8367  en1  8371  fodomr  8462  unxpdomlem3  8517  fineqvlem  8525  f1opwfi  8621  fsuppcolem  8657  fsuppco  8658  mapfienlem1  8661  mapfienlem2  8662  supub  8716  suplub  8717  ordtypelem2  8776  ordtypelem3  8777  ordtypelem6  8780  ordtypelem7  8781  wemapso2lem  8809  wdom2d  8837  brwdom3  8839  ixpiunwdom  8848  inf3lem2  8884  inf3lem6  8888  oancom  8906  infdifsn  8912  cantnfp1lem3  8935  cantnflem3  8946  cantnflem4  8947  oef1o  8953  cnfcom3  8959  tctr  8974  tz9.12lem3  9010  scottex  9106  cardid2  9174  infxpenlem  9231  acni3  9265  cardaleph  9307  iscard3  9311  dfac5lem4  9344  dfac5lem5  9345  kmlem1  9368  cofsmo  9487  fin4en1  9527  enfin2i  9539  fin23lem28  9558  fin23lem38  9567  isf32lem6  9576  enfin1ai  9602  hsmexlem2  9645  hsmexlem4  9647  domtriomlem  9660  axdc2lem  9666  axdc3lem2  9669  ac6num  9697  zorn2lem2  9715  brdom3  9746  alephval2  9790  alephreg  9800  pwcfsdom  9801  smobeth  9804  fpwwe2lem6  9853  fpwwe2lem13  9860  canthp1lem2  9871  pwfseqlem3  9878  hargch  9891  winalim2  9914  gchina  9917  inar1  9993  0npi  10100  mulclpi  10111  mulcanpi  10118  nlt1pi  10124  nqereu  10147  prcdnq  10211  prnmax  10213  ltresr2  10359  axrnegex  10380  axpre-sup  10387  eluz2gt1  12132  1nuz2  12136  zsupss  12149  rpgt0  12216  ixxss1  12570  ixxss2  12571  ixxss12  12572  lbioo  12583  ubioo  12584  iccss2  12621  iccssico2  12624  elfzuz3  12719  serge0  13237  expge0  13278  expge1  13279  expaddzlem  13285  hashrabsn1  13546  hashfun  13609  cshinj  14033  relexpuzrel  14270  shftfn  14291  sqrlem6  14466  rlimss  14718  lo1dm  14735  o1dm  14746  rlimrege0  14795  fsumf1o  14938  fsumge0  15008  incexc2  15051  supcvg  15069  fprodf1o  15158  divalglem9  15610  bitsfzolem  15641  bitsf1  15653  gcdcllem1  15706  bezout  15745  nprm  15886  dvdsprm  15901  coprm  15909  dfphi2  15965  phimullem  15970  phisum  15981  expnprm  16092  prmreclem2  16107  prmreclem5  16110  1arith  16117  4sqlem18  16152  vdwnnlem3  16187  ramtlecl  16190  rami  16205  0ram  16210  ramub1lem1  16216  prmgaplem5  16245  acsfiel  16795  isacs1i  16798  catlid  16824  catrid  16825  fullfo  17052  fthf1  17057  fthoppc  17063  invfuc  17114  prslem  17411  posi  17430  dlatmjdi  17674  pslem  17686  tsrlin  17699  cnvtsr  17702  tsrdir  17718  mndid  17783  mhmf  17820  mhmlin  17822  mhm0  17823  mndind  17846  grpinvex  17913  grplinv  17951  mulgz  18051  mulgdirlem  18054  mulgdir  18055  mulgass  18060  nsgbi  18106  nmzbi  18115  ghmf  18145  ghmlin  18146  conjnsg  18177  gimf1o  18186  gagrpid  18207  gaf  18208  gaass  18210  psgnunilem5  18395  psgnunilem5OLD  18396  odid  18440  odf1o2  18471  gexid  18479  sylow1lem4  18499  pj1id  18595  efgredeu  18650  ablcmn  18684  cmncom  18694  mulgdi  18717  torsubg  18742  cyggenod2  18772  cygctb  18778  ghmcyg  18782  dprdf1o  18916  ablfacrplem  18949  ablfaclem2  18970  ablfac2  18973  crngmgp  19040  rhmmhm  19209  rhmghm  19212  drngunit  19242  drngmgp  19249  drngid  19251  subrgss  19271  subrg1cl  19278  issubdrg  19295  cntzsdrg  19315  abvge0  19330  srngcnv  19358  lmhmlin  19541  lmimf1o  19569  lvecdrng  19611  lspsolvlem  19648  islbs3  19661  lbsextlem3  19666  2idlcpbl  19740  nzrnz  19766  opprnzr  19771  rrgeq0i  19795  domneq0  19803  domnrrg  19806  drngdomn  19809  fldidom  19811  assalem  19822  mplsubrglem  19945  mplcoe1  19971  mplbas2  19976  opsrtoslem2  19990  mplelsfi  19996  coe1mul2  20155  zringunit  20352  prmirredlem  20357  znidomb  20425  cygzn  20434  psgndiflemB  20461  pjf  20574  frlmsslsp  20657  frlmlbs  20658  f1lindf  20683  pmatcoe1fsupp  21028  toponuni  21241  tpsuni  21263  mretopd  21419  neips  21440  neiptoptop  21458  neiptopnei  21459  perflp  21481  perfi  21482  cnf  21573  cnpf  21574  cnpimaex  21583  cnima  21592  t0sep  21651  t1ficld  21654  hausnei  21655  pnrmcld  21669  cnrmi  21687  cmpcov  21716  tgcmp  21728  hauscmplem  21733  connclo  21742  1stcclb  21771  2ndcdisj  21783  llyi  21801  nllyi  21802  ptpjpre1  21898  ptpjcn  21938  ptpjopn  21939  ptclsg  21942  dfac14  21945  txdis1cn  21962  pthaus  21965  hauseqlcld  21973  txkgen  21979  xkococn  21987  txconn  22016  hmeocnvcn  22088  fbssfi  22164  filss  22180  uffixfr  22250  flimneiss  22293  flimelbas  22295  flimfnfcls  22355  alexsubb  22373  alexsubALT  22378  ptcmplem2  22380  ptcmplem3  22381  ptcmplem4  22382  tmdgsum2  22423  ghmcnp  22441  tgpt0  22445  qustgplem  22447  istdrg2  22504  vscacn  22512  tvctdrg  22519  uspreg  22601  ucncn  22612  neipcfilu  22623  cuspcvg  22628  psmetxrge0  22641  isxmet2d  22655  prdsxmetlem  22696  imasdsf1olem  22701  xmstopn  22779  mstopn  22780  stdbdxmet  22843  prdsxmslem2  22857  nrgabv  22988  nmvs  23003  nvclvec  23024  nmoge0  23048  nghmcl  23054  nmoi  23055  nghmghm  23061  nmhmlmhm  23076  nmhmnghm  23077  icccmp  23151  xrge0gsumle  23159  metds0  23176  metdstri  23177  metdsre  23179  metdseq0  23180  metdscnlem  23181  metnrmlem1a  23184  icopnfcnv  23264  xrhmeo  23268  pcoval1  23335  cvslvec  23447  cvsunit  23453  cphreccllem  23500  cphsscph  23572  cmetcvg  23606  lmle  23622  cmscmet  23667  cmetcusp1  23674  hlcph  23685  minveclem4  23753  ivthlem3  23772  ovolmge0  23796  ovolicc1  23835  ovolicc2lem3  23838  ovolicc2lem5  23840  dyadmbl  23919  i1ff  23995  i1frn  23996  i1fima2  23998  itg2monolem1  24069  dvnres  24246  c1liplem1  24311  c1lip2  24313  dvge0  24321  lhop1lem  24328  itgsubstlem  24363  fta1glem2  24478  fta1b  24481  plyf  24506  plypf1  24520  plyadd  24525  plymul  24526  coeeu  24533  dgrlem  24537  coeid  24546  elqaalem3  24628  aareccl  24633  eff1olem  24848  relogf1o  24866  logdmn0  24939  logcnlem2  24942  logcnlem3  24943  efopnlem1  24955  efopnlem2  24956  logtayl2  24961  cxpcn3lem  25044  cxpcn3  25045  logbgcd1irr  25088  atandmneg  25200  atandmcj  25203  efiatan2  25211  cosatan  25215  cosatanne0  25216  dvatan  25229  areage0  25258  cxp2lim  25271  jensenlem2  25282  jensen  25283  eldmgm  25316  dmgmaddn0  25317  dmlogdmgm  25318  lgamgulmlem2  25324  lgamgulmlem3  25325  lgamgulmlem5  25327  lgambdd  25331  lgamucov  25332  ftalem3  25369  efnnfsumcl  25397  efchtdvds  25453  sqff1o  25476  fsumdvdsdiaglem  25477  dvdsppwf1o  25480  dvdsflf1o  25481  musum  25485  muinv  25487  dvdsmulf1o  25488  lgsfle1  25599  lgsle1  25605  lgsdirprm  25624  lgsne0  25628  lgseisenlem3  25670  lgseisenlem4  25671  lgsquadlem1  25673  lgsquadlem2  25674  chebbnd1  25765  chtppilim  25768  chpchtlim  25772  chpo1ub  25773  dchrmusumlema  25786  dchrvmasumlem1  25788  dchrisum0lema  25807  dchrisum0lem2a  25810  logsqvma  25835  selberg3lem2  25851  pntrsumo1  25858  pnt2  25906  ostthlem1  25920  ostth3  25931  axtgcgrrflx  25965  axtgcgrid  25966  axtgsegcon  25967  axtg5seg  25968  axtgbtwnid  25969  axtgpasch  25970  axtgcont1  25971  tglng  26049  axcontlem7  26474  axcontlem10  26477  upgrle  26593  umgredg2  26603  lfgredgge2  26627  usgredg2ALT  26693  usgr1vr  26755  usgrexmpledg  26762  upgrres1  26813  fusgrvtxfi  26819  vtxnbuvtx  26891  cusgrcplgr  26920  vdumgr0  26980  vtxdgoddnumeven  27053  trlres  27203  trlresOLD  27205  usgr2pth  27268  cyclispthon  27305  clwwlknlen  27562  clwwnonrepclwwnon  27896  clwwnonrepclwwnonOLD  27897  2clwwlk2  27900  ablocom  28117  phpar2  28392  cbncms  28435  hlph  28459  hcaucvg  28757  hlimconvi  28762  shaddcl  28788  shmulcl  28789  chlimi  28805  chcompl  28813  choc1  28900  nmopre  29443  cnopc  29486  lnopl  29487  unop  29488  hmop  29495  cnfnc  29503  lnfnl  29504  nlelshi  29633  cnlnadjlem5  29644  elpjidm  29757  mdslle1i  29890  mdslle2i  29891  atcv0  29915  chpssati  29936  fovcld  30164  aciunf1lem  30186  padct  30231  ssnnssfz  30286  ressprs  30400  oduprs  30401  resspos  30404  resstos  30405  tleile  30406  ogrpinvOLD  30460  ogrpinv0le  30461  ogrpsub  30462  ogrpaddlt  30463  cyc3evpm  30495  isarchi3  30514  archirng  30515  archirngz  30516  archiabllem1a  30518  archiabllem1b  30519  archiabllem2a  30521  archiabllem2c  30522  archiabllem2b  30523  archiabl  30525  orngsqr  30588  ornglmulle  30589  orngrmulle  30590  ofldtos  30595  ofldlt1  30597  ofldchr  30598  suborng  30599  subofld  30600  isarchiofld  30601  nn0omnd  30625  sradrng  30649  extdg1id  30714  madjusmdetlem4  30769  qtophaus  30776  crefi  30787  cmpcref  30790  cmppcmp  30798  pcmplfin  30800  tpr2rico  30831  rge0scvg  30868  zrhunitpreima  30895  qqhrhm  30906  esummono  30989  gsumesum  30994  esumrnmpt2  31003  esumpinfval  31008  esumpcvgval  31013  esumpmono  31014  0elsiga  31050  sigaclcu  31053  issgon  31059  inelpisys  31090  ldsysgenld  31096  ldgenpisyslem1  31099  sxuni  31129  isrnmeas  31136  measvuni  31150  measssd  31151  ddemeas  31172  imambfm  31197  elmbfmvol2  31202  dya2icoseg2  31213  omssubaddlem  31234  omssubadd  31235  carsgsigalem  31250  pmeasmono  31259  sibfinima  31274  oddpwdc  31289  oddpwdcv  31290  eulerpartlemf  31305  eulerpartlemt  31306  eulerpartlemr  31309  eulerpartlemgvv  31311  eulerpartlemgs2  31315  fiblem  31334  probtot  31348  ballotlem4  31434  ballotlem5  31435  ballotlemfrc  31462  ballotlemirc  31467  ballotth  31473  hgt750lemb  31607  bnj642  31699  bnj643  31700  bnj645  31701  bnj707  31706  bnj1379  31782  bnj1538  31806  bnj110  31809  bnj93  31814  bnj906  31881  bnj1006  31910  bnj1110  31931  bnj1121  31934  bnj1204  31961  bnj1321  31976  bnj1364  31977  bnj1398  31983  bnj1450  31999  bnj1312  32007  bnj1501  32016  bnj1523  32020  subfacp1lem3  32051  subfacp1lem5  32053  pconncn  32093  connpconn  32104  cvmcov  32132  cvmliftlem1  32154  cvmliftlem10  32163  cvmlift2lem11  32182  cvmlift2lem12  32183  msubff1  32360  mvhf1  32363  mthmpps  32386  mclspps  32388  fundmpss  32566  tfisg  32613  frpoinsg  32639  frinsg  32645  sltval2  32721  funpartfun  32962  fnetg  33251  neibastop1  33265  filnetlem3  33286  onint1  33354  bj-nnf1  33810  bj-elid2  33976  icorempo  34111  pibt2  34176  wl-nfeqfb  34255  phpreu  34354  fin2solem  34356  fin2so  34357  lindsenlbs  34365  matunitlindflem1  34366  matunitlindflem2  34367  matunitlindf  34368  ptrest  34369  poimirlem1  34371  poimirlem2  34372  poimirlem3  34373  poimirlem4  34374  poimirlem5  34375  poimirlem6  34376  poimirlem7  34377  poimirlem8  34378  poimirlem9  34379  poimirlem10  34380  poimirlem11  34381  poimirlem12  34382  poimirlem13  34383  poimirlem14  34384  poimirlem15  34385  poimirlem16  34386  poimirlem17  34387  poimirlem18  34388  poimirlem19  34389  poimirlem20  34390  poimirlem21  34391  poimirlem22  34392  poimirlem23  34393  poimirlem24  34394  poimirlem26  34396  poimirlem27  34397  poimirlem29  34399  poimirlem31  34401  mblfinlem2  34408  dvtan  34420  itg2gt0cn  34425  ftc1anclem7  34451  ftc1anclem8  34452  ftc1anc  34453  cover2  34468  indexa  34487  istotbnd3  34528  sstotbnd2  34531  sstotbnd  34532  totbndss  34534  equivtotbnd  34535  isbnd3  34541  totbndbnd  34546  equivbnd  34547  prdsbnd  34550  prdstotbnd  34551  heibor  34578  zrdivrng  34710  crngocom  34758  isfld2  34762  dmncrng  34813  eqvrelrel  35314  disjrel  35445  prter2  35499  toycom  35591  lsateln0  35613  lpssat  35631  lssat  35634  oposlem  35800  olop  35832  omllaw  35861  cvlexch1  35946  dihpN  37954  mapdordlem2  38255  prjspertr  38700  nacsfg  38735  nacsfix  38742  mzpindd  38776  diophrw  38789  diophrex  38806  rexzrexnn0  38835  pell1234qrdich  38892  rmspecnonsq  38938  rmspecfund  38940  rmspecpos  38947  monotoddzzfi  38973  ltrmxnn0  38980  rmxnn  38982  jm2.23  39027  jm3.1lem2  39049  dnnumch3  39081  lnmlssfg  39114  lnmlmic  39122  lnrlnm  39147  lnr2i  39150  lpirlnr  39151  hbtlem6  39163  hbt  39164  mnccoe  39172  idomrootle  39229  proot1mul  39233  proot1hash  39234  deg1mhm  39241  ntrneifv2  39831  grucollcld  40009  mnurndlem1  40030  simpg2nsg  40068  fincygsubgodexd  40086  radcnvrat  40100  binomcxplemdvbinom  40139  binomcxplemcvg  40140  binomcxplemnotnn0  40142  ordelordALT  40328  2uasbanh  40352  ordelordALTVD  40658  elixpconstg  40812  rabidim2  40827  foelrnf  40906  disjinfi  40913  supminfxr2  41210  sumnnodd  41376  stoweidlem7  41757  stoweidlem14  41764  stoweidlem16  41766  stoweidlem24  41774  stoweidlem31  41781  stoweidlem54  41804  wallispilem3  41817  fourierdlem42  41899  fourierdlem48  41904  fourierdlem51  41907  fourierdlem64  41920  fourierdlem76  41932  fourierdlem79  41935  fourierdlem81  41937  fourierdlem87  41943  etransclem28  42012  etransclem32  42016  sge0fodjrnlem  42163  hoidmvlelem3  42344  pimrecltpos  42452  pimrecltneg  42466  issmflem  42469  smfaddlem1  42504  smfsuplem1  42550  smfsuplem3  42552  smflimsuplem7  42565  smfliminflem  42569  nfunsnafv  42781  faovcl  42839  tz6.12-2-afv2  42876  tz6.12i-afv2  42882  sprel  43048  evendiv2z  43199  oddp1div2z  43200  2dvdseven  43220  2ndvdsodd  43222  perfectALTVlem1  43288  sbgoldbm  43351  clintopcllaw  43516  0ringbas  43540  rnghmmgmhm  43563  uzlidlring  43598  rnghmsubcsetclem1  43644  rngccatidALTV  43658  zrinitorngc  43669  zrtermorngc  43670  rhmsubcsetclem1  43690  funcringcsetcALTV2lem7  43711  ringccatidALTV  43721  funcringcsetclem7ALTV  43734  irinitoringc  43738  zrtermoringc  43739  fldhmsubc  43753  fldhmsubcALTV  43771  ssnn0ssfz  43795  el0ldepsnzr  43923  regt1loggt0  43998  elbigodm  44017  fllogbd  44022  rrx2xpref1o  44107  elsetrecslem  44202