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

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

Proof of Theorem simprrr
StepHypRef Expression
1 simpr 485 . 2 ((𝜒𝜃) → 𝜃)
21ad2antll 727 1 ((𝜑 ∧ (𝜓 ∧ (𝜒𝜃))) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 397
This theorem is referenced by:  prproe  4861  f1prex  7224  fliftfun  7251  fprresex  8208  wfrlem17OLD  8238  mapdom2  9025  domunfican  9197  fofinf1o  9204  finsschain  9236  wemaplem3  9417  oemapvali  9553  iunfictbso  9983  enfin2i  10190  fin1a2s  10283  distrlem4pr  10895  mulcmpblnr  10940  prsrlem1  10941  addsrmo  10942  mulsrmo  10943  divdivdiv  11789  divsubdiv  11804  lediv12a  11981  xralrple  13052  seqcaopr  13873  leexp2r  14005  hashbclem  14276  wrd2ind  14542  cshwidxmod  14622  rtrclreclem4  14879  relexpindlem  14881  rtrclind  14883  rlimresb  15381  summo  15536  fsum2dlem  15589  prodmo  15753  fprod2dlem  15797  bezoutlem3  16356  bezoutlem4  16357  qredeu  16468  coprmproddvdslem  16472  prmdvdsncoprmbd  16536  pcqmul  16659  pcadd  16695  pockthg  16712  ramub1lem2  16833  cshwsdisj  16905  mreexexlem4d  17461  issubc3  17669  cofucl  17708  setcmon  17907  setcepi  17908  drsdirfi  18128  poslubmo  18234  posglbmo  18235  grpridd  18464  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  27331  hlcgreu  27358  mirreu3  27394  opphllem  27475  oppperpex  27493  lnperpex  27543  trgcopy  27544  iscgra1  27550  cgraswap  27560  cgracom  27562  cgratr  27563  flatcgra  27564  acopyeu  27574  ax5seglem9  27684  ax5seg  27685  axcontlem8  27718  axcontlem12  27722  upgrclwlkcompim  28527  wwlksnextwrd  28640  2pthfrgr  29026  frgrnbnb  29035  ablo4  29290  smcnlem  29437  pjhthmo  30042  1stpreimas  31414  xrge0tsmsd  31693  locfinref  32195  xpinpreima2  32261  qqhval2  32336  dya2iocnrect  32654  orvcgteel  32840  orvclteel  32845  cnpconn  33597  txpconn  33599  connpconn  33602  pconnpi1  33604  iccllysconn  33617  rellysconn  33618  cvmcov2  33642  cvmliftmolem2  33649  cvmliftmo  33651  cvmliftlem15  33665  cvmliftpht  33685  cvmlift3lem2  33687  naddssim  34228  cgrextend  34488  btwnouttr2  34502  btwnexch2  34503  cgrxfr  34535  lineext  34556  btwnconn1lem5  34571  btwnconn1lem13  34579  btwnconn3  34583  segletr  34594  segleantisym  34595  outsideofeq  34610  outsidele  34612  lineunray  34627  refssfne  34725  neibastop2lem  34727  neibastop2  34728  unblimceq0lem  34864  knoppndvlem22  34891  mblfinlem3  36012  mblfinlem4  36013  cnambfre  36021  itg2addnclem  36024  areacirclem5  36065  istotbnd3  36125  crngm4  36357  cvlcvr1  37696  4atlem12  37970  cdlemb  38152  paddasslem10  38187  paddasslem12  38189  paddasslem13  38190  lhpexle3lem  38369  cdlemd4  38559  cdlemefs32sn1aw  38772  cdleme43fsv1snlem  38778  cdleme32d  38802  cdleme32f  38804  cdleme40m  38825  cdleme40n  38826  cdleme50trn2  38909  cdlemftr3  38923  cdlemm10N  39476  dihvalcqpre  39593  dihopelvalcpre  39606  dihmeetlem1N  39648  dihglblem5apreN  39649  dihmeetlem4preN  39664  dihjat1lem  39786  mapd0  40023  mapdh9a  40147  nna4b4nsq  40863  mzpmfp  40935  mzpcompact2lem  40939  diophin  40960  pellexlem3  41019  pellex  41023  pell14qrmulcl  41051  jm2.19lem3  41180  jm2.25  41188  jm2.27b  41195  fnwe2lem2  41243  hbtlem2  41316  hbtlem5  41320  gsumws3  42233  gsumws4  42234  mnuprdlem1  42316  mnuprdlem2  42317  mnuprdlem4  42319  fnchoice  42998  stoweidlem53  44047  stoweidlem61  44055  qndenserrnbllem  44288  bgoldbtbnd  45750  prsthinc  46823
  Copyright terms: Public domain W3C validator