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

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

Proof of Theorem simprrr
StepHypRef Expression
1 simpr 479 . 2 ((𝜒𝜃) → 𝜃)
21ad2antll 767 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 197  df-an 385
This theorem is referenced by:  prproe  4574  f1prex  6690  fliftfun  6713  grpridd  7027  wfrlem17  7588  mapdom2  8284  domunfican  8386  fofinf1o  8394  finsschain  8426  wemaplem3  8606  oemapvali  8742  iunfictbso  9098  enfin2i  9306  fin1a2s  9399  distrlem4pr  10011  mulcmpblnr  10055  prsrlem1  10056  addsrmo  10057  mulsrmo  10058  divdivdiv  10889  divsubdiv  10904  lediv12a  11079  xralrple  12200  seqcaopr  13003  leexp2r  13083  hashbclem  13399  wrd2ind  13648  cshwidxmod  13720  rtrclreclem4  13971  relexpindlem  13973  rtrclind  13975  rlimresb  14466  summo  14618  fsum2dlem  14671  prodmo  14836  fprod2dlem  14880  bezoutlem3  15431  bezoutlem4  15432  qredeu  15545  coprmproddvdslem  15549  pcqmul  15731  pcadd  15766  pockthg  15783  ramub1lem2  15904  cshwsdisj  15978  mreexexlem4d  16480  issubc3  16681  cofucl  16720  setcmon  16909  setcepi  16910  drsdirfi  17110  poslubmo  17318  posglbmo  17319  ghmpreima  17854  gaorber  17912  psgnunilem4  18088  psgneu  18097  odcau  18190  pgpssslw  18200  fislw  18211  lsmsubm  18239  efgsfo  18323  pgpfac1  18650  pgpfaclem2  18652  pgpfaclem3  18653  unitgrp  18838  islmodd  19042  lmodprop2d  19098  lsspropd  19190  lbsextlem4  19334  assapropd  19500  evlslem1  19688  mdetunilem8  20598  mdetmul  20602  ppttop  20984  epttop  20986  restbas  21135  iscnp4  21240  cnpco  21244  nrmsep  21334  regsep2  21353  ordthauslem  21360  1stcfb  21421  2ndcctbss  21431  2ndcdisj  21432  2ndcomap  21434  dis2ndc  21436  1stcelcls  21437  nlly2i  21452  islly2  21460  hausllycmp  21470  lly1stc  21472  comppfsc  21508  1stckgenlem  21529  ptbasin  21553  txcls  21580  ptcnp  21598  txlly  21612  txnlly  21613  txtube  21616  txcmplem1  21617  txcmplem2  21618  xkococnlem  21635  basqtop  21687  regr1lem  21715  kqreglem1  21717  kqreglem2  21718  kqnrmlem1  21719  kqnrmlem2  21720  reghmph  21769  nrmhmph  21770  filuni  21861  rnelfmlem  21928  fmufil  21935  fclscf  22001  fclsfnflim  22003  flimfnfcls  22004  uffclsflim  22007  cnpfcfi  22016  cnpfcf  22017  alexsublem  22020  alexsubALTlem3  22025  tgpconncompeqg  22087  ghmcnp  22090  qustgplem  22096  blssps  22401  blss  22402  blcld  22482  metequiv2  22487  met2ndci  22499  prdsxmslem2  22506  txmetcnp  22524  nlmvscnlem1  22662  xrge0tsms  22809  ipcnlem1  23215  iscmet3  23262  cmetss  23284  minveclem3  23371  pmltpc  23390  ovolscalem2  23453  ovolicc2lem5  23460  ovolicc2  23461  nulmbl2  23475  ioombl1  23501  uniioombllem6  23527  uniioombl  23528  vitalilem3  23549  i1faddlem  23630  mbfmullem  23662  itg2const2  23678  itg2split  23686  lhop2  23948  dvfsumrlim  23964  itgsubst  23982  plydivex  24222  plyexmo  24238  ulmbdd  24322  cxploglim  24874  dchrptlem2  25160  lgsquad2lem2  25280  2sqlem5  25317  dchrvmasumif  25362  rpvmasum2  25371  dchrisum0re  25372  dchrisum0lem3  25378  dchrisum0  25379  dchrmusum  25383  dchrvmasum  25384  pntibndlem3  25451  pntlemp  25469  ostth3  25497  legtrid  25656  hlcgreu  25683  mirreu3  25719  opphllem  25797  oppperpex  25815  lnperpex  25865  trgcopy  25866  iscgra1  25872  cgraswap  25882  cgracom  25884  cgratr  25885  acopyeu  25895  ax5seglem9  25987  ax5seg  25988  axcontlem8  26021  axcontlem12  26025  upgrclwlkcompim  26858  wlkwwlkfun  26975  wwlksnextwrd  26986  2pthfrgr  27409  frgrnbnb  27418  ablo4  27684  smcnlem  27832  pjhthmo  28441  1stpreimas  29763  xrge0tsmsd  30065  locfinref  30188  xpinpreima2  30233  qqhval2  30306  dya2iocnrect  30623  orvcgteel  30809  orvclteel  30814  cnpconn  31490  txpconn  31492  connpconn  31495  pconnpi1  31497  iccllysconn  31510  rellysconn  31511  cvmcov2  31535  cvmliftmolem2  31542  cvmliftmo  31544  cvmliftlem15  31558  cvmliftpht  31578  cvmlift3lem2  31580  nosupbnd1lem1  32131  nosupbnd2  32139  conway  32187  cgrextend  32392  btwnouttr2  32406  btwnexch2  32407  cgrxfr  32439  lineext  32460  btwnconn1lem5  32475  btwnconn1lem13  32483  btwnconn3  32487  segletr  32498  segleantisym  32499  outsideofeq  32514  outsidele  32516  lineunray  32531  refssfne  32630  neibastop2lem  32632  neibastop2  32633  unblimceq0lem  32774  knoppndvlem22  32801  mblfinlem3  33730  mblfinlem4  33731  cnambfre  33740  itg2addnclem  33743  areacirclem5  33786  istotbnd3  33852  crngm4  34084  cvlcvr1  35098  4atlem12  35370  cdlemb  35552  paddasslem10  35587  paddasslem12  35589  paddasslem13  35590  lhpexle3lem  35769  cdlemd4  35960  cdlemefs32sn1aw  36173  cdleme43fsv1snlem  36179  cdleme32d  36203  cdleme32f  36205  cdleme40m  36226  cdleme40n  36227  cdleme50trn2  36310  cdlemftr3  36324  cdlemm10N  36878  dihvalcqpre  36995  dihopelvalcpre  37008  dihmeetlem1N  37050  dihglblem5apreN  37051  dihmeetlem4preN  37066  dihjat1lem  37188  mapd0  37425  mapdh9a  37550  mzpmfp  37781  mzpcompact2lem  37785  diophin  37807  pellexlem3  37866  pellex  37870  pell14qrmulcl  37898  jm2.19lem3  38029  jm2.25  38037  jm2.27b  38044  fnwe2lem2  38092  hbtlem2  38165  hbtlem5  38169  gsumws3  38970  gsumws4  38971  fnchoice  39656  stoweidlem53  40742  stoweidlem61  40750  qndenserrnbllem  40986  bgoldbtbnd  42176
  Copyright terms: Public domain W3C validator