MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simprrr Structured version   Visualization version   GIF version

Theorem simprrr 801
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simprrr ((𝜑 ∧ (𝜓 ∧ (𝜒𝜃))) → 𝜃)

Proof of Theorem simprrr
StepHypRef Expression
1 simpr 476 . 2 ((𝜒𝜃) → 𝜃)
21ad2antll 761 1 ((𝜑 ∧ (𝜓 ∧ (𝜒𝜃))) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  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:  f1prex  6439  fliftfun  6462  grpridd  6772  wfrlem17  7318  mapdom2  8016  domunfican  8118  fofinf1o  8126  finsschain  8156  wemaplem3  8336  oemapvali  8464  iunfictbso  8820  enfin2i  9026  fin1a2s  9119  distrlem4pr  9727  mulcmpblnr  9771  prsrlem1  9772  addsrmo  9773  mulsrmo  9774  divdivdiv  10605  divsubdiv  10620  lediv12a  10795  xralrple  11910  seqcaopr  12700  leexp2r  12780  hashbclem  13093  wrd2ind  13329  cshwidxmod  13400  rtrclreclem4  13649  relexpindlem  13651  rtrclind  13653  rlimresb  14144  summo  14295  fsum2dlem  14343  prodmo  14505  fprod2dlem  14549  bezoutlem3  15096  bezoutlem4  15097  qredeu  15210  coprmproddvdslem  15214  pcqmul  15396  pcadd  15431  pockthg  15448  ramub1lem2  15569  cshwsdisj  15643  mreexexlem4d  16130  issubc3  16332  cofucl  16371  setcmon  16560  setcepi  16561  drsdirfi  16761  poslubmo  16969  posglbmo  16970  ghmpreima  17505  gaorber  17564  psgnunilem4  17740  psgneu  17749  odcau  17842  pgpssslw  17852  fislw  17863  lsmsubm  17891  efgsfo  17975  pgpfac1  18302  pgpfaclem2  18304  pgpfaclem3  18305  unitgrp  18490  islmodd  18692  lmodprop2d  18748  lsspropd  18838  lbsextlem4  18982  assapropd  19148  evlslem1  19336  mdetunilem8  20244  mdetmul  20248  ppttop  20621  epttop  20623  restbas  20772  iscnp4  20877  cnpco  20881  nrmsep  20971  regsep2  20990  ordthauslem  20997  1stcfb  21058  2ndcctbss  21068  2ndcdisj  21069  2ndcomap  21071  dis2ndc  21073  1stcelcls  21074  nlly2i  21089  islly2  21097  hausllycmp  21107  lly1stc  21109  comppfsc  21145  1stckgenlem  21166  ptbasin  21190  txcls  21217  ptcnp  21235  txlly  21249  txnlly  21250  txtube  21253  txcmplem1  21254  txcmplem2  21255  xkococnlem  21272  basqtop  21324  regr1lem  21352  kqreglem1  21354  kqreglem2  21355  kqnrmlem1  21356  kqnrmlem2  21357  reghmph  21406  nrmhmph  21407  filuni  21499  rnelfmlem  21566  fmufil  21573  fclscf  21639  fclsfnflim  21641  flimfnfcls  21642  uffclsflim  21645  cnpfcfi  21654  cnpfcf  21655  alexsublem  21658  alexsubALTlem3  21663  tgpconcompeqg  21725  ghmcnp  21728  qustgplem  21734  blssps  22039  blss  22040  blcld  22120  metequiv2  22125  met2ndci  22137  prdsxmslem2  22144  txmetcnp  22162  nlmvscnlem1  22300  xrge0tsms  22445  ipcnlem1  22852  iscmet3  22899  cmetss  22921  minveclem3  23008  pmltpc  23026  ovolscalem2  23089  ovolicc2lem5  23096  ovolicc2  23097  nulmbl2  23111  ioombl1  23137  uniioombllem6  23162  uniioombl  23163  vitalilem3  23185  i1faddlem  23266  mbfmullem  23298  itg2const2  23314  itg2split  23322  lhop2  23582  dvfsumrlim  23598  itgsubst  23616  plydivex  23856  plyexmo  23872  ulmbdd  23956  cxploglim  24504  dchrptlem2  24790  lgsquad2lem2  24910  2sqlem5  24947  dchrvmasumif  24992  rpvmasum2  25001  dchrisum0re  25002  dchrisum0lem3  25008  dchrisum0  25009  dchrmusum  25013  dchrvmasum  25014  pntibndlem3  25081  pntlemp  25099  ostth3  25127  legtrid  25286  hlcgreu  25313  mirreu3  25349  opphllem  25427  oppperpex  25445  lnperpex  25495  trgcopy  25496  iscgra1  25502  cgraswap  25512  cgracom  25514  cgratr  25515  acopyeu  25525  ax5seglem9  25617  ax5seg  25618  axcontlem8  25651  axcontlem12  25655  wlkiswwlkfun  26245  wwlkextwrd  26256  usg2spthonot0  26416  frgranbnb  26547  frgrancvvdeqlemC  26566  ablo4  26788  smcnlem  26936  pjhthmo  27545  1stpreimas  28866  xrge0tsmsd  29116  locfinref  29236  xpinpreima2  29281  qqhval2  29354  dya2iocnrect  29670  orvcgteel  29856  orvclteel  29861  cnpcon  30466  txpcon  30468  conpcon  30471  pconpi1  30473  iccllyscon  30486  rellyscon  30487  cvmcov2  30511  cvmliftmolem2  30518  cvmliftmo  30520  cvmliftlem15  30534  cvmliftpht  30554  cvmlift3lem2  30556  cgrextend  31285  btwnouttr2  31299  btwnexch2  31300  cgrxfr  31332  lineext  31353  btwnconn1lem5  31368  btwnconn1lem13  31376  btwnconn3  31380  segletr  31391  segleantisym  31392  outsideofeq  31407  outsidele  31409  lineunray  31424  refssfne  31523  neibastop2lem  31525  neibastop2  31526  unblimceq0lem  31667  knoppndvlem22  31694  mblfinlem3  32618  mblfinlem4  32619  cnambfre  32628  itg2addnclem  32631  areacirclem5  32674  istotbnd3  32740  crngm4  32972  cvlcvr1  33644  4atlem12  33916  cdlemb  34098  paddasslem10  34133  paddasslem12  34135  paddasslem13  34136  lhpexle3lem  34315  cdlemd4  34506  cdlemefs32sn1aw  34720  cdleme43fsv1snlem  34726  cdleme32d  34750  cdleme32f  34752  cdleme40m  34773  cdleme40n  34774  cdleme50trn2  34857  cdlemftr3  34871  cdlemm10N  35425  dihvalcqpre  35542  dihopelvalcpre  35555  dihmeetlem1N  35597  dihglblem5apreN  35598  dihmeetlem4preN  35613  dihjat1lem  35735  mapd0  35972  mapdh9a  36097  mzpmfp  36328  mzpcompact2lem  36332  diophin  36354  pellexlem3  36413  pellex  36417  pell14qrmulcl  36445  jm2.19lem3  36576  jm2.25  36584  jm2.27b  36591  fnwe2lem2  36639  hbtlem2  36713  hbtlem5  36717  gsumws3  37521  gsumws4  37522  fnchoice  38211  stoweidlem53  38946  stoweidlem61  38954  qndenserrnbllem  39190  bgoldbtbnd  40225  upgrclwlkcompim  40988  wlkwwlkfun  41092  wwlksnextwrd  41103  2pthfrgr  41454  frgrnbnb  41463  frgrncvvdeqlemC  41478
  Copyright terms: Public domain W3C validator