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

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

Proof of Theorem simprrr
StepHypRef Expression
1 simpr 486 . 2 ((𝜒𝜃) → 𝜃)
21ad2antll 728 1 ((𝜑 ∧ (𝜓 ∧ (𝜒𝜃))) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 398
This theorem is referenced by:  prproe  4862  f1prex  7225  fliftfun  7252  fprresex  8209  wfrlem17OLD  8239  mapdom2  9026  domunfican  9198  fofinf1o  9205  finsschain  9237  wemaplem3  9418  oemapvali  9554  iunfictbso  9984  enfin2i  10191  fin1a2s  10284  distrlem4pr  10896  mulcmpblnr  10941  prsrlem1  10942  addsrmo  10943  mulsrmo  10944  divdivdiv  11790  divsubdiv  11805  lediv12a  11982  xralrple  13053  seqcaopr  13874  leexp2r  14006  hashbclem  14277  wrd2ind  14543  cshwidxmod  14623  rtrclreclem4  14880  relexpindlem  14882  rtrclind  14884  rlimresb  15382  summo  15537  fsum2dlem  15590  prodmo  15754  fprod2dlem  15798  bezoutlem3  16357  bezoutlem4  16358  qredeu  16469  coprmproddvdslem  16473  prmdvdsncoprmbd  16537  pcqmul  16660  pcadd  16696  pockthg  16713  ramub1lem2  16834  cshwsdisj  16906  mreexexlem4d  17462  issubc3  17670  cofucl  17709  setcmon  17908  setcepi  17909  drsdirfi  18129  poslubmo  18235  posglbmo  18236  grpridd  18465  ghmpreima  18962  gaorber  19020  psgnunilem4  19211  psgneu  19220  odcau  19315  pgpssslw  19325  fislw  19336  lsmsubm  19364  efgsfo  19450  pgpfac1  19788  pgpfaclem2  19790  pgpfaclem3  19791  unitgrp  20019  islmodd  20251  lmodprop2d  20307  lsspropd  20401  lbsextlem4  20545  assapropd  21198  evlslem1  21414  mdetunilem8  21890  mdetmul  21894  ppttop  22279  epttop  22281  restbas  22431  iscnp4  22536  cnpco  22540  nrmsep  22630  regsep2  22649  ordthauslem  22656  1stcfb  22718  2ndcctbss  22728  2ndcdisj  22729  2ndcomap  22731  dis2ndc  22733  1stcelcls  22734  nlly2i  22749  islly2  22757  hausllycmp  22767  lly1stc  22769  comppfsc  22805  1stckgenlem  22826  ptbasin  22850  txcls  22877  ptcnp  22895  txlly  22909  txnlly  22910  txtube  22913  txcmplem1  22914  txcmplem2  22915  xkococnlem  22932  basqtop  22984  regr1lem  23012  kqreglem1  23014  kqreglem2  23015  kqnrmlem1  23016  kqnrmlem2  23017  reghmph  23066  nrmhmph  23067  filuni  23158  rnelfmlem  23225  fmufil  23232  fclscf  23298  fclsfnflim  23300  flimfnfcls  23301  uffclsflim  23304  cnpfcfi  23313  cnpfcf  23314  alexsublem  23317  alexsubALTlem3  23322  tgpconncompeqg  23385  ghmcnp  23388  qustgplem  23394  blssps  23699  blss  23700  blcld  23783  metequiv2  23788  met2ndci  23800  prdsxmslem2  23807  txmetcnp  23825  nlmvscnlem1  23972  xrge0tsms  24119  ipcnlem1  24531  iscmet3  24579  metsscmetcld  24601  minveclem3  24715  pmltpc  24736  ovolscalem2  24800  ovolicc2lem5  24807  ovolicc2  24808  nulmbl2  24822  ioombl1  24848  uniioombllem6  24874  uniioombl  24875  vitalilem3  24896  i1faddlem  24979  mbfmullem  25012  itg2const2  25028  itg2split  25036  lhop2  25301  dvfsumrlim  25317  itgsubst  25335  plydivex  25579  plyexmo  25595  ulmbdd  25679  cxploglim  26249  dchrptlem2  26535  lgsquad2lem2  26655  2sqlem5  26692  dchrvmasumif  26773  rpvmasum2  26782  dchrisum0re  26783  dchrisum0lem3  26789  dchrisum0  26790  dchrmusum  26794  dchrvmasum  26795  pntibndlem3  26862  pntlemp  26880  ostth3  26908  nosupbday  26975  nosupbnd1lem1  26978  nosupbnd2  26986  noinfbday  26990  noinfbnd1lem1  26993  noinfbnd2  27001  conway  27060  madebdaylemlrcut  27146  legtrid  27319  hlcgreu  27346  mirreu3  27382  opphllem  27463  oppperpex  27481  lnperpex  27531  trgcopy  27532  iscgra1  27538  cgraswap  27548  cgracom  27550  cgratr  27551  flatcgra  27552  acopyeu  27562  ax5seglem9  27672  ax5seg  27673  axcontlem8  27706  axcontlem12  27710  upgrclwlkcompim  28515  wwlksnextwrd  28628  2pthfrgr  29014  frgrnbnb  29023  ablo4  29278  smcnlem  29425  pjhthmo  30030  1stpreimas  31402  xrge0tsmsd  31681  locfinref  32183  xpinpreima2  32249  qqhval2  32324  dya2iocnrect  32642  orvcgteel  32828  orvclteel  32833  cnpconn  33585  txpconn  33587  connpconn  33590  pconnpi1  33592  iccllysconn  33605  rellysconn  33606  cvmcov2  33630  cvmliftmolem2  33637  cvmliftmo  33639  cvmliftlem15  33653  cvmliftpht  33673  cvmlift3lem2  33675  naddssim  34216  cgrextend  34479  btwnouttr2  34493  btwnexch2  34494  cgrxfr  34526  lineext  34547  btwnconn1lem5  34562  btwnconn1lem13  34570  btwnconn3  34574  segletr  34585  segleantisym  34586  outsideofeq  34601  outsidele  34603  lineunray  34618  refssfne  34716  neibastop2lem  34718  neibastop2  34719  unblimceq0lem  34855  knoppndvlem22  34882  mblfinlem3  36003  mblfinlem4  36004  cnambfre  36012  itg2addnclem  36015  areacirclem5  36056  istotbnd3  36116  crngm4  36348  cvlcvr1  37687  4atlem12  37961  cdlemb  38143  paddasslem10  38178  paddasslem12  38180  paddasslem13  38181  lhpexle3lem  38360  cdlemd4  38550  cdlemefs32sn1aw  38763  cdleme43fsv1snlem  38769  cdleme32d  38793  cdleme32f  38795  cdleme40m  38816  cdleme40n  38817  cdleme50trn2  38900  cdlemftr3  38914  cdlemm10N  39467  dihvalcqpre  39584  dihopelvalcpre  39597  dihmeetlem1N  39639  dihglblem5apreN  39640  dihmeetlem4preN  39655  dihjat1lem  39777  mapd0  40014  mapdh9a  40138  nna4b4nsq  40832  mzpmfp  40904  mzpcompact2lem  40908  diophin  40929  pellexlem3  40988  pellex  40992  pell14qrmulcl  41020  jm2.19lem3  41149  jm2.25  41157  jm2.27b  41164  fnwe2lem2  41212  hbtlem2  41285  hbtlem5  41289  gsumws3  42202  gsumws4  42203  mnuprdlem1  42285  mnuprdlem2  42286  mnuprdlem4  42288  fnchoice  42967  stoweidlem53  44004  stoweidlem61  44012  qndenserrnbllem  44245  bgoldbtbnd  45701  prsthinc  46774
  Copyright terms: Public domain W3C validator