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 488 . 2 ((𝜒𝜃) → 𝜃)
21ad2antll 728 1 ((𝜑 ∧ (𝜓 ∧ (𝜒𝜃))) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  prproe  4823  f1prex  7030  fliftfun  7055  wfrlem17  7963  mapdom2  8681  domunfican  8784  fofinf1o  8792  finsschain  8824  wemaplem3  9005  oemapvali  9140  iunfictbso  9534  enfin2i  9737  fin1a2s  9830  distrlem4pr  10442  mulcmpblnr  10487  prsrlem1  10488  addsrmo  10489  mulsrmo  10490  divdivdiv  11335  divsubdiv  11350  lediv12a  11527  xralrple  12593  seqcaopr  13410  leexp2r  13541  hashbclem  13813  wrd2ind  14083  cshwidxmod  14163  rtrclreclem4  14418  relexpindlem  14420  rtrclind  14422  rlimresb  14920  summo  15072  fsum2dlem  15123  prodmo  15288  fprod2dlem  15332  bezoutlem3  15885  bezoutlem4  15886  qredeu  15998  coprmproddvdslem  16002  pcqmul  16186  pcadd  16221  pockthg  16238  ramub1lem2  16359  cshwsdisj  16430  mreexexlem4d  16916  issubc3  17117  cofucl  17156  setcmon  17345  setcepi  17346  drsdirfi  17546  poslubmo  17754  posglbmo  17755  grpridd  17883  ghmpreima  18378  gaorber  18436  psgnunilem4  18623  psgneu  18632  odcau  18727  pgpssslw  18737  fislw  18748  lsmsubm  18776  efgsfo  18863  pgpfac1  19200  pgpfaclem2  19202  pgpfaclem3  19203  unitgrp  19415  islmodd  19635  lmodprop2d  19691  lsspropd  19784  lbsextlem4  19928  assapropd  20096  evlslem1  20290  mdetunilem8  21223  mdetmul  21227  ppttop  21610  epttop  21612  restbas  21761  iscnp4  21866  cnpco  21870  nrmsep  21960  regsep2  21979  ordthauslem  21986  1stcfb  22048  2ndcctbss  22058  2ndcdisj  22059  2ndcomap  22061  dis2ndc  22063  1stcelcls  22064  nlly2i  22079  islly2  22087  hausllycmp  22097  lly1stc  22099  comppfsc  22135  1stckgenlem  22156  ptbasin  22180  txcls  22207  ptcnp  22225  txlly  22239  txnlly  22240  txtube  22243  txcmplem1  22244  txcmplem2  22245  xkococnlem  22262  basqtop  22314  regr1lem  22342  kqreglem1  22344  kqreglem2  22345  kqnrmlem1  22346  kqnrmlem2  22347  reghmph  22396  nrmhmph  22397  filuni  22488  rnelfmlem  22555  fmufil  22562  fclscf  22628  fclsfnflim  22630  flimfnfcls  22631  uffclsflim  22634  cnpfcfi  22643  cnpfcf  22644  alexsublem  22647  alexsubALTlem3  22652  tgpconncompeqg  22715  ghmcnp  22718  qustgplem  22724  blssps  23029  blss  23030  blcld  23110  metequiv2  23115  met2ndci  23127  prdsxmslem2  23134  txmetcnp  23152  nlmvscnlem1  23290  xrge0tsms  23437  ipcnlem1  23847  iscmet3  23895  metsscmetcld  23917  minveclem3  24031  pmltpc  24052  ovolscalem2  24116  ovolicc2lem5  24123  ovolicc2  24124  nulmbl2  24138  ioombl1  24164  uniioombllem6  24190  uniioombl  24191  vitalilem3  24212  i1faddlem  24295  mbfmullem  24327  itg2const2  24343  itg2split  24351  lhop2  24616  dvfsumrlim  24632  itgsubst  24650  plydivex  24891  plyexmo  24907  ulmbdd  24991  cxploglim  25561  dchrptlem2  25847  lgsquad2lem2  25967  2sqlem5  26004  dchrvmasumif  26085  rpvmasum2  26094  dchrisum0re  26095  dchrisum0lem3  26101  dchrisum0  26102  dchrmusum  26106  dchrvmasum  26107  pntibndlem3  26174  pntlemp  26192  ostth3  26220  legtrid  26383  hlcgreu  26410  mirreu3  26446  opphllem  26527  oppperpex  26545  lnperpex  26595  trgcopy  26596  iscgra1  26602  cgraswap  26612  cgracom  26614  cgratr  26615  flatcgra  26616  acopyeu  26626  ax5seglem9  26729  ax5seg  26730  axcontlem8  26763  axcontlem12  26767  upgrclwlkcompim  27568  wwlksnextwrd  27681  2pthfrgr  28067  frgrnbnb  28076  ablo4  28331  smcnlem  28478  pjhthmo  29083  1stpreimas  30447  xrge0tsmsd  30719  locfinref  31135  xpinpreima2  31177  qqhval2  31250  dya2iocnrect  31566  orvcgteel  31752  orvclteel  31757  cnpconn  32504  txpconn  32506  connpconn  32509  pconnpi1  32511  iccllysconn  32524  rellysconn  32525  cvmcov2  32549  cvmliftmolem2  32556  cvmliftmo  32558  cvmliftlem15  32572  cvmliftpht  32592  cvmlift3lem2  32594  nosupbnd1lem1  33235  nosupbnd2  33243  conway  33291  cgrextend  33496  btwnouttr2  33510  btwnexch2  33511  cgrxfr  33543  lineext  33564  btwnconn1lem5  33579  btwnconn1lem13  33587  btwnconn3  33591  segletr  33602  segleantisym  33603  outsideofeq  33618  outsidele  33620  lineunray  33635  refssfne  33733  neibastop2lem  33735  neibastop2  33736  unblimceq0lem  33872  knoppndvlem22  33899  mblfinlem3  35008  mblfinlem4  35009  cnambfre  35017  itg2addnclem  35020  areacirclem5  35061  istotbnd3  35121  crngm4  35353  cvlcvr1  36547  4atlem12  36820  cdlemb  37002  paddasslem10  37037  paddasslem12  37039  paddasslem13  37040  lhpexle3lem  37219  cdlemd4  37409  cdlemefs32sn1aw  37622  cdleme43fsv1snlem  37628  cdleme32d  37652  cdleme32f  37654  cdleme40m  37675  cdleme40n  37676  cdleme50trn2  37759  cdlemftr3  37773  cdlemm10N  38326  dihvalcqpre  38443  dihopelvalcpre  38456  dihmeetlem1N  38498  dihglblem5apreN  38499  dihmeetlem4preN  38514  dihjat1lem  38636  mapd0  38873  mapdh9a  38997  mzpmfp  39544  mzpcompact2lem  39548  diophin  39569  pellexlem3  39628  pellex  39632  pell14qrmulcl  39660  jm2.19lem3  39788  jm2.25  39796  jm2.27b  39803  fnwe2lem2  39851  hbtlem2  39924  hbtlem5  39928  gsumws3  40761  gsumws4  40762  mnuprdlem1  40840  mnuprdlem2  40841  mnuprdlem4  40843  fnchoice  41518  stoweidlem53  42561  stoweidlem61  42569  qndenserrnbllem  42802  bgoldbtbnd  44193
  Copyright terms: Public domain W3C validator