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

Theorem simprrr 778
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 725 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 208  df-an 397
This theorem is referenced by:  prproe  4830  f1prex  7031  fliftfun  7054  wfrlem17  7962  mapdom2  8677  domunfican  8780  fofinf1o  8788  finsschain  8820  wemaplem3  9001  oemapvali  9136  iunfictbso  9529  enfin2i  9732  fin1a2s  9825  distrlem4pr  10437  mulcmpblnr  10482  prsrlem1  10483  addsrmo  10484  mulsrmo  10485  divdivdiv  11330  divsubdiv  11345  lediv12a  11522  xralrple  12588  seqcaopr  13397  leexp2r  13528  hashbclem  13800  wrd2ind  14075  cshwidxmod  14155  rtrclreclem4  14410  relexpindlem  14412  rtrclind  14414  rlimresb  14912  summo  15064  fsum2dlem  15115  prodmo  15280  fprod2dlem  15324  bezoutlem3  15879  bezoutlem4  15880  qredeu  15992  coprmproddvdslem  15996  pcqmul  16180  pcadd  16215  pockthg  16232  ramub1lem2  16353  cshwsdisj  16422  mreexexlem4d  16908  issubc3  17109  cofucl  17148  setcmon  17337  setcepi  17338  drsdirfi  17538  poslubmo  17746  posglbmo  17747  grpridd  17875  ghmpreima  18320  gaorber  18378  psgnunilem4  18556  psgneu  18565  odcau  18660  pgpssslw  18670  fislw  18681  lsmsubm  18709  efgsfo  18796  pgpfac1  19133  pgpfaclem2  19135  pgpfaclem3  19136  unitgrp  19348  islmodd  19571  lmodprop2d  19627  lsspropd  19720  lbsextlem4  19864  assapropd  20031  evlslem1  20225  mdetunilem8  21158  mdetmul  21162  ppttop  21545  epttop  21547  restbas  21696  iscnp4  21801  cnpco  21805  nrmsep  21895  regsep2  21914  ordthauslem  21921  1stcfb  21983  2ndcctbss  21993  2ndcdisj  21994  2ndcomap  21996  dis2ndc  21998  1stcelcls  21999  nlly2i  22014  islly2  22022  hausllycmp  22032  lly1stc  22034  comppfsc  22070  1stckgenlem  22091  ptbasin  22115  txcls  22142  ptcnp  22160  txlly  22174  txnlly  22175  txtube  22178  txcmplem1  22179  txcmplem2  22180  xkococnlem  22197  basqtop  22249  regr1lem  22277  kqreglem1  22279  kqreglem2  22280  kqnrmlem1  22281  kqnrmlem2  22282  reghmph  22331  nrmhmph  22332  filuni  22423  rnelfmlem  22490  fmufil  22497  fclscf  22563  fclsfnflim  22565  flimfnfcls  22566  uffclsflim  22569  cnpfcfi  22578  cnpfcf  22579  alexsublem  22582  alexsubALTlem3  22587  tgpconncompeqg  22649  ghmcnp  22652  qustgplem  22658  blssps  22963  blss  22964  blcld  23044  metequiv2  23049  met2ndci  23061  prdsxmslem2  23068  txmetcnp  23086  nlmvscnlem1  23224  xrge0tsms  23371  ipcnlem1  23777  iscmet3  23825  metsscmetcld  23847  minveclem3  23961  pmltpc  23980  ovolscalem2  24044  ovolicc2lem5  24051  ovolicc2  24052  nulmbl2  24066  ioombl1  24092  uniioombllem6  24118  uniioombl  24119  vitalilem3  24140  i1faddlem  24223  mbfmullem  24255  itg2const2  24271  itg2split  24279  lhop2  24541  dvfsumrlim  24557  itgsubst  24575  plydivex  24815  plyexmo  24831  ulmbdd  24915  cxploglim  25483  dchrptlem2  25769  lgsquad2lem2  25889  2sqlem5  25926  dchrvmasumif  26007  rpvmasum2  26016  dchrisum0re  26017  dchrisum0lem3  26023  dchrisum0  26024  dchrmusum  26028  dchrvmasum  26029  pntibndlem3  26096  pntlemp  26114  ostth3  26142  legtrid  26305  hlcgreu  26332  mirreu3  26368  opphllem  26449  oppperpex  26467  lnperpex  26517  trgcopy  26518  iscgra1  26524  cgraswap  26534  cgracom  26536  cgratr  26537  flatcgra  26538  acopyeu  26548  ax5seglem9  26651  ax5seg  26652  axcontlem8  26685  axcontlem12  26689  upgrclwlkcompim  27490  wwlksnextwrd  27603  2pthfrgr  27991  frgrnbnb  28000  ablo4  28255  smcnlem  28402  pjhthmo  29007  1stpreimas  30368  xrge0tsmsd  30620  locfinref  31005  xpinpreima2  31050  qqhval2  31123  dya2iocnrect  31439  orvcgteel  31625  orvclteel  31630  cnpconn  32375  txpconn  32377  connpconn  32380  pconnpi1  32382  iccllysconn  32395  rellysconn  32396  cvmcov2  32420  cvmliftmolem2  32427  cvmliftmo  32429  cvmliftlem15  32443  cvmliftpht  32463  cvmlift3lem2  32465  nosupbnd1lem1  33106  nosupbnd2  33114  conway  33162  cgrextend  33367  btwnouttr2  33381  btwnexch2  33382  cgrxfr  33414  lineext  33435  btwnconn1lem5  33450  btwnconn1lem13  33458  btwnconn3  33462  segletr  33473  segleantisym  33474  outsideofeq  33489  outsidele  33491  lineunray  33506  refssfne  33604  neibastop2lem  33606  neibastop2  33607  unblimceq0lem  33743  knoppndvlem22  33770  mblfinlem3  34813  mblfinlem4  34814  cnambfre  34822  itg2addnclem  34825  areacirclem5  34868  istotbnd3  34932  crngm4  35164  cvlcvr1  36357  4atlem12  36630  cdlemb  36812  paddasslem10  36847  paddasslem12  36849  paddasslem13  36850  lhpexle3lem  37029  cdlemd4  37219  cdlemefs32sn1aw  37432  cdleme43fsv1snlem  37438  cdleme32d  37462  cdleme32f  37464  cdleme40m  37485  cdleme40n  37486  cdleme50trn2  37569  cdlemftr3  37583  cdlemm10N  38136  dihvalcqpre  38253  dihopelvalcpre  38266  dihmeetlem1N  38308  dihglblem5apreN  38309  dihmeetlem4preN  38324  dihjat1lem  38446  mapd0  38683  mapdh9a  38807  mzpmfp  39224  mzpcompact2lem  39228  diophin  39249  pellexlem3  39308  pellex  39312  pell14qrmulcl  39340  jm2.19lem3  39468  jm2.25  39476  jm2.27b  39483  fnwe2lem2  39531  hbtlem2  39604  hbtlem5  39608  gsumws3  40430  gsumws4  40431  mnuprdlem1  40488  mnuprdlem2  40489  mnuprdlem4  40491  fnchoice  41166  stoweidlem53  42219  stoweidlem61  42227  qndenserrnbllem  42460  bgoldbtbnd  43821
  Copyright terms: Public domain W3C validator