Theorem simprrr 782

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simprrr	⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜃)

Proof of Theorem simprrr

Step	Hyp	Ref	Expression
1		simpr 484	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜃)
2	1	ad2antll 730	1 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  prproe  4862  f1prex  7233  fliftfun  7261  fprresex  8255  nnaordex2  8570  naddssim  8616  mapdom2  9081  domunfican  9227  fofinf1o  9237  finsschain  9264  wemaplem3  9458  oemapvali  9598  iunfictbso  10029  enfin2i  10236  fin1a2s  10329  distrlem4pr  10942  mulcmpblnr  10987  prsrlem1  10988  addsrmo  10989  mulsrmo  10990  divdivdiv  11847  divsubdiv  11862  lediv12a  12040  xralrple  13125  seqcaopr  13967  leexp2r  14102  hashbclem  14380  wrd2ind  14651  cshwidxmod  14731  rtrclreclem4  14989  relexpindlem  14991  rtrclind  14993  rlimresb  15493  summo  15645  fsum2dlem  15698  prodmo  15864  fprod2dlem  15908  bezoutlem3  16473  bezoutlem4  16474  qredeu  16590  coprmproddvdslem  16594  prmdvdsncoprmbd  16659  pcqmul  16786  pcadd  16822  pockthg  16839  ramub1lem2  16960  cshwsdisj  17031  mreexexlem4d  17575  issubc3  17778  cofucl  17817  setcmon  18016  setcepi  18017  drsdirfi  18233  poslubmo  18337  posglbmo  18338  grprida  18605  ghmpreima  19172  gaorber  19242  psgnunilem4  19431  psgneu  19440  odcau  19538  pgpssslw  19548  fislw  19559  lsmsubm  19587  efgsfo  19673  pgpfac1  20016  pgpfaclem2  20018  pgpfaclem3  20019  unitgrp  20324  islmodd  20822  lmodprop2d  20880  lsspropd  20974  lbsextlem4  21121  assapropd  21832  evlslem1  22042  mdetunilem8  22568  mdetmul  22572  ppttop  22956  epttop  22958  restbas  23107  iscnp4  23212  cnpco  23216  nrmsep  23306  regsep2  23325  ordthauslem  23332  1stcfb  23394  2ndcctbss  23404  2ndcdisj  23405  2ndcomap  23407  dis2ndc  23409  1stcelcls  23410  nlly2i  23425  islly2  23433  hausllycmp  23443  lly1stc  23445  comppfsc  23481  1stckgenlem  23502  ptbasin  23526  txcls  23553  ptcnp  23571  txlly  23585  txnlly  23586  txtube  23589  txcmplem1  23590  txcmplem2  23591  xkococnlem  23608  basqtop  23660  regr1lem  23688  kqreglem1  23690  kqreglem2  23691  kqnrmlem1  23692  kqnrmlem2  23693  reghmph  23742  nrmhmph  23743  filuni  23834  rnelfmlem  23901  fmufil  23908  fclscf  23974  fclsfnflim  23976  flimfnfcls  23977  uffclsflim  23980  cnpfcfi  23989  cnpfcf  23990  alexsublem  23993  alexsubALTlem3  23998  tgpconncompeqg  24061  ghmcnp  24064  qustgplem  24070  blssps  24373  blss  24374  blcld  24454  metequiv2  24459  met2ndci  24471  prdsxmslem2  24478  txmetcnp  24496  nlmvscnlem1  24635  xrge0tsms  24784  ipcnlem1  25206  iscmet3  25254  metsscmetcld  25276  minveclem3  25390  pmltpc  25412  ovolscalem2  25476  ovolicc2lem5  25483  ovolicc2  25484  nulmbl2  25498  ioombl1  25524  uniioombllem6  25550  uniioombl  25551  vitalilem3  25572  i1faddlem  25655  mbfmullem  25687  itg2const2  25703  itg2split  25711  lhop2  25981  dvfsumrlim  25999  itgsubst  26017  plydivex  26266  plyexmo  26282  ulmbdd  26368  cxploglim  26949  dchrptlem2  27237  lgsquad2lem2  27357  2sqlem5  27394  dchrvmasumif  27475  rpvmasum2  27484  dchrisum0re  27485  dchrisum0lem3  27491  dchrisum0  27492  dchrmusum  27496  dchrvmasum  27497  pntibndlem3  27564  pntlemp  27582  ostth3  27610  nosupbday  27678  nosupbnd1lem1  27681  nosupbnd2  27689  noinfbday  27693  noinfbnd1lem1  27696  noinfbnd2  27704  conway  27780  madebdaylemlrcut  27900  mulsproplem9  28125  mulsuniflem  28150  uzsind  28406  bdayfinbndlem1  28468  readdscl  28500  legtrid  28668  hlcgreu  28695  mirreu3  28731  opphllem  28812  oppperpex  28830  lnperpex  28880  trgcopy  28881  iscgra1  28887  cgraswap  28897  cgracom  28899  cgratr  28900  flatcgra  28901  acopyeu  28911  ax5seglem9  29015  ax5seg  29016  axcontlem8  29049  axcontlem12  29053  upgrclwlkcompim  29859  wwlksnextwrd  29975  2pthfrgr  30364  frgrnbnb  30373  ablo4  30630  smcnlem  30777  pjhthmo  31382  1stpreimas  32788  xrge0tsmsd  33159  locfinref  34011  xpinpreima2  34077  qqhval2  34152  dya2iocnrect  34451  orvcgteel  34638  orvclteel  34643  cnpconn  35437  txpconn  35439  connpconn  35442  pconnpi1  35444  iccllysconn  35457  rellysconn  35458  cvmcov2  35482  cvmliftmolem2  35489  cvmliftmo  35491  cvmliftlem15  35505  cvmliftpht  35525  cvmlift3lem2  35527  cgrextend  36215  btwnouttr2  36229  btwnexch2  36230  cgrxfr  36262  lineext  36283  btwnconn1lem5  36298  btwnconn1lem13  36306  btwnconn3  36310  segletr  36321  segleantisym  36322  outsideofeq  36337  outsidele  36339  lineunray  36354  refssfne  36565  neibastop2lem  36567  neibastop2  36568  weiunpo  36672  unblimceq0lem  36719  knoppndvlem22  36746  mblfinlem3  37873  mblfinlem4  37874  cnambfre  37882  itg2addnclem  37885  areacirclem5  37926  istotbnd3  37985  crngm4  38217  cvlcvr1  39678  4atlem12  39951  cdlemb  40133  paddasslem10  40168  paddasslem12  40170  paddasslem13  40171  lhpexle3lem  40350  cdlemd4  40540  cdlemefs32sn1aw  40753  cdleme43fsv1snlem  40759  cdleme32d  40783  cdleme32f  40785  cdleme40m  40806  cdleme40n  40807  cdleme50trn2  40890  cdlemftr3  40904  cdlemm10N  41457  dihvalcqpre  41574  dihopelvalcpre  41587  dihmeetlem1N  41629  dihglblem5apreN  41630  dihmeetlem4preN  41645  dihjat1lem  41767  mapd0  42004  mapdh9a  42128  nna4b4nsq  42981  mzpmfp  43067  mzpcompact2lem  43071  diophin  43092  pellexlem3  43151  pellex  43155  pell14qrmulcl  43183  jm2.19lem3  43311  jm2.25  43319  jm2.27b  43326  fnwe2lem2  43371  hbtlem2  43444  hbtlem5  43448  gsumws3  44515  gsumws4  44516  mnuprdlem1  44591  mnuprdlem2  44592  mnuprdlem4  44594  fnchoice  45352  stoweidlem53  46374  stoweidlem61  46382  qndenserrnbllem  46615  bgoldbtbnd  48132  cycldlenngric  48251  grtrimap  48271  isubgr3stgrlem6  48294  prsthinc  49786