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

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

Proof of Theorem simprrr
StepHypRef Expression
1 simpr 476 . 2 ((𝜒𝜃) → 𝜃)
21ad2antll 765 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  4466  f1prex  6579  fliftfun  6602  grpridd  6916  wfrlem17  7476  mapdom2  8172  domunfican  8274  fofinf1o  8282  finsschain  8314  wemaplem3  8494  oemapvali  8619  iunfictbso  8975  enfin2i  9181  fin1a2s  9274  distrlem4pr  9886  mulcmpblnr  9930  prsrlem1  9931  addsrmo  9932  mulsrmo  9933  divdivdiv  10764  divsubdiv  10779  lediv12a  10954  xralrple  12074  seqcaopr  12878  leexp2r  12958  hashbclem  13274  wrd2ind  13523  cshwidxmod  13595  rtrclreclem4  13845  relexpindlem  13847  rtrclind  13849  rlimresb  14340  summo  14492  fsum2dlem  14545  prodmo  14710  fprod2dlem  14754  bezoutlem3  15305  bezoutlem4  15306  qredeu  15419  coprmproddvdslem  15423  pcqmul  15605  pcadd  15640  pockthg  15657  ramub1lem2  15778  cshwsdisj  15852  mreexexlem4d  16354  issubc3  16556  cofucl  16595  setcmon  16784  setcepi  16785  drsdirfi  16985  poslubmo  17193  posglbmo  17194  ghmpreima  17729  gaorber  17787  psgnunilem4  17963  psgneu  17972  odcau  18065  pgpssslw  18075  fislw  18086  lsmsubm  18114  efgsfo  18198  pgpfac1  18525  pgpfaclem2  18527  pgpfaclem3  18528  unitgrp  18713  islmodd  18917  lmodprop2d  18973  lsspropd  19065  lbsextlem4  19209  assapropd  19375  evlslem1  19563  mdetunilem8  20473  mdetmul  20477  ppttop  20859  epttop  20861  restbas  21010  iscnp4  21115  cnpco  21119  nrmsep  21209  regsep2  21228  ordthauslem  21235  1stcfb  21296  2ndcctbss  21306  2ndcdisj  21307  2ndcomap  21309  dis2ndc  21311  1stcelcls  21312  nlly2i  21327  islly2  21335  hausllycmp  21345  lly1stc  21347  comppfsc  21383  1stckgenlem  21404  ptbasin  21428  txcls  21455  ptcnp  21473  txlly  21487  txnlly  21488  txtube  21491  txcmplem1  21492  txcmplem2  21493  xkococnlem  21510  basqtop  21562  regr1lem  21590  kqreglem1  21592  kqreglem2  21593  kqnrmlem1  21594  kqnrmlem2  21595  reghmph  21644  nrmhmph  21645  filuni  21736  rnelfmlem  21803  fmufil  21810  fclscf  21876  fclsfnflim  21878  flimfnfcls  21879  uffclsflim  21882  cnpfcfi  21891  cnpfcf  21892  alexsublem  21895  alexsubALTlem3  21900  tgpconncompeqg  21962  ghmcnp  21965  qustgplem  21971  blssps  22276  blss  22277  blcld  22357  metequiv2  22362  met2ndci  22374  prdsxmslem2  22381  txmetcnp  22399  nlmvscnlem1  22537  xrge0tsms  22684  ipcnlem1  23090  iscmet3  23137  cmetss  23159  minveclem3  23246  pmltpc  23265  ovolscalem2  23328  ovolicc2lem5  23335  ovolicc2  23336  nulmbl2  23350  ioombl1  23376  uniioombllem6  23402  uniioombl  23403  vitalilem3  23424  i1faddlem  23505  mbfmullem  23537  itg2const2  23553  itg2split  23561  lhop2  23823  dvfsumrlim  23839  itgsubst  23857  plydivex  24097  plyexmo  24113  ulmbdd  24197  cxploglim  24749  dchrptlem2  25035  lgsquad2lem2  25155  2sqlem5  25192  dchrvmasumif  25237  rpvmasum2  25246  dchrisum0re  25247  dchrisum0lem3  25253  dchrisum0  25254  dchrmusum  25258  dchrvmasum  25259  pntibndlem3  25326  pntlemp  25344  ostth3  25372  legtrid  25531  hlcgreu  25558  mirreu3  25594  opphllem  25672  oppperpex  25690  lnperpex  25740  trgcopy  25741  iscgra1  25747  cgraswap  25757  cgracom  25759  cgratr  25760  acopyeu  25770  ax5seglem9  25862  ax5seg  25863  axcontlem8  25896  axcontlem12  25900  upgrclwlkcompim  26733  wlkwwlkfun  26849  wwlksnextwrd  26860  2pthfrgr  27264  frgrnbnb  27273  ablo4  27532  smcnlem  27680  pjhthmo  28289  1stpreimas  29611  xrge0tsmsd  29913  locfinref  30036  xpinpreima2  30081  qqhval2  30154  dya2iocnrect  30471  orvcgteel  30657  orvclteel  30662  cnpconn  31338  txpconn  31340  connpconn  31343  pconnpi1  31345  iccllysconn  31358  rellysconn  31359  cvmcov2  31383  cvmliftmolem2  31390  cvmliftmo  31392  cvmliftlem15  31406  cvmliftpht  31426  cvmlift3lem2  31428  nosupbnd1lem1  31979  nosupbnd2  31987  conway  32035  cgrextend  32240  btwnouttr2  32254  btwnexch2  32255  cgrxfr  32287  lineext  32308  btwnconn1lem5  32323  btwnconn1lem13  32331  btwnconn3  32335  segletr  32346  segleantisym  32347  outsideofeq  32362  outsidele  32364  lineunray  32379  refssfne  32478  neibastop2lem  32480  neibastop2  32481  unblimceq0lem  32622  knoppndvlem22  32649  mblfinlem3  33578  mblfinlem4  33579  cnambfre  33588  itg2addnclem  33591  areacirclem5  33634  istotbnd3  33700  crngm4  33932  cvlcvr1  34944  4atlem12  35216  cdlemb  35398  paddasslem10  35433  paddasslem12  35435  paddasslem13  35436  lhpexle3lem  35615  cdlemd4  35806  cdlemefs32sn1aw  36019  cdleme43fsv1snlem  36025  cdleme32d  36049  cdleme32f  36051  cdleme40m  36072  cdleme40n  36073  cdleme50trn2  36156  cdlemftr3  36170  cdlemm10N  36724  dihvalcqpre  36841  dihopelvalcpre  36854  dihmeetlem1N  36896  dihglblem5apreN  36897  dihmeetlem4preN  36912  dihjat1lem  37034  mapd0  37271  mapdh9a  37396  mzpmfp  37627  mzpcompact2lem  37631  diophin  37653  pellexlem3  37712  pellex  37716  pell14qrmulcl  37744  jm2.19lem3  37875  jm2.25  37883  jm2.27b  37890  fnwe2lem2  37938  hbtlem2  38011  hbtlem5  38015  gsumws3  38816  gsumws4  38817  fnchoice  39502  stoweidlem53  40588  stoweidlem61  40596  qndenserrnbllem  40832  bgoldbtbnd  42022
  Copyright terms: Public domain W3C validator