Theorem simprrr 781

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 729	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  4871  f1prex  7261  fliftfun  7289  fprresex  8291  nnaordex2  8605  naddssim  8651  mapdom2  9117  domunfican  9278  fofinf1o  9289  finsschain  9316  wemaplem3  9507  oemapvali  9643  iunfictbso  10073  enfin2i  10280  fin1a2s  10373  distrlem4pr  10985  mulcmpblnr  11030  prsrlem1  11031  addsrmo  11032  mulsrmo  11033  divdivdiv  11889  divsubdiv  11904  lediv12a  12082  xralrple  13171  seqcaopr  14010  leexp2r  14145  hashbclem  14423  wrd2ind  14694  cshwidxmod  14774  rtrclreclem4  15033  relexpindlem  15035  rtrclind  15037  rlimresb  15537  summo  15689  fsum2dlem  15742  prodmo  15908  fprod2dlem  15952  bezoutlem3  16517  bezoutlem4  16518  qredeu  16634  coprmproddvdslem  16638  prmdvdsncoprmbd  16703  pcqmul  16830  pcadd  16866  pockthg  16883  ramub1lem2  17004  cshwsdisj  17075  mreexexlem4d  17614  issubc3  17817  cofucl  17856  setcmon  18055  setcepi  18056  drsdirfi  18272  poslubmo  18376  posglbmo  18377  grprida  18608  ghmpreima  19176  gaorber  19246  psgnunilem4  19433  psgneu  19442  odcau  19540  pgpssslw  19550  fislw  19561  lsmsubm  19589  efgsfo  19675  pgpfac1  20018  pgpfaclem2  20020  pgpfaclem3  20021  unitgrp  20298  islmodd  20778  lmodprop2d  20836  lsspropd  20930  lbsextlem4  21077  assapropd  21787  evlslem1  21995  mdetunilem8  22512  mdetmul  22516  ppttop  22900  epttop  22902  restbas  23051  iscnp4  23156  cnpco  23160  nrmsep  23250  regsep2  23269  ordthauslem  23276  1stcfb  23338  2ndcctbss  23348  2ndcdisj  23349  2ndcomap  23351  dis2ndc  23353  1stcelcls  23354  nlly2i  23369  islly2  23377  hausllycmp  23387  lly1stc  23389  comppfsc  23425  1stckgenlem  23446  ptbasin  23470  txcls  23497  ptcnp  23515  txlly  23529  txnlly  23530  txtube  23533  txcmplem1  23534  txcmplem2  23535  xkococnlem  23552  basqtop  23604  regr1lem  23632  kqreglem1  23634  kqreglem2  23635  kqnrmlem1  23636  kqnrmlem2  23637  reghmph  23686  nrmhmph  23687  filuni  23778  rnelfmlem  23845  fmufil  23852  fclscf  23918  fclsfnflim  23920  flimfnfcls  23921  uffclsflim  23924  cnpfcfi  23933  cnpfcf  23934  alexsublem  23937  alexsubALTlem3  23942  tgpconncompeqg  24005  ghmcnp  24008  qustgplem  24014  blssps  24318  blss  24319  blcld  24399  metequiv2  24404  met2ndci  24416  prdsxmslem2  24423  txmetcnp  24441  nlmvscnlem1  24580  xrge0tsms  24729  ipcnlem1  25151  iscmet3  25199  metsscmetcld  25221  minveclem3  25335  pmltpc  25357  ovolscalem2  25421  ovolicc2lem5  25428  ovolicc2  25429  nulmbl2  25443  ioombl1  25469  uniioombllem6  25495  uniioombl  25496  vitalilem3  25517  i1faddlem  25600  mbfmullem  25632  itg2const2  25648  itg2split  25656  lhop2  25926  dvfsumrlim  25944  itgsubst  25962  plydivex  26211  plyexmo  26227  ulmbdd  26313  cxploglim  26894  dchrptlem2  27182  lgsquad2lem2  27302  2sqlem5  27339  dchrvmasumif  27420  rpvmasum2  27429  dchrisum0re  27430  dchrisum0lem3  27436  dchrisum0  27437  dchrmusum  27441  dchrvmasum  27442  pntibndlem3  27509  pntlemp  27527  ostth3  27555  nosupbday  27623  nosupbnd1lem1  27626  nosupbnd2  27634  noinfbday  27638  noinfbnd1lem1  27641  noinfbnd2  27649  conway  27717  madebdaylemlrcut  27816  mulsproplem9  28033  mulsuniflem  28058  uzsind  28299  readdscl  28356  legtrid  28524  hlcgreu  28551  mirreu3  28587  opphllem  28668  oppperpex  28686  lnperpex  28736  trgcopy  28737  iscgra1  28743  cgraswap  28753  cgracom  28755  cgratr  28756  flatcgra  28757  acopyeu  28767  ax5seglem9  28870  ax5seg  28871  axcontlem8  28904  axcontlem12  28908  upgrclwlkcompim  29717  wwlksnextwrd  29833  2pthfrgr  30219  frgrnbnb  30228  ablo4  30485  smcnlem  30632  pjhthmo  31237  1stpreimas  32635  xrge0tsmsd  33008  locfinref  33837  xpinpreima2  33903  qqhval2  33978  dya2iocnrect  34278  orvcgteel  34465  orvclteel  34470  cnpconn  35217  txpconn  35219  connpconn  35222  pconnpi1  35224  iccllysconn  35237  rellysconn  35238  cvmcov2  35262  cvmliftmolem2  35269  cvmliftmo  35271  cvmliftlem15  35285  cvmliftpht  35305  cvmlift3lem2  35307  cgrextend  35991  btwnouttr2  36005  btwnexch2  36006  cgrxfr  36038  lineext  36059  btwnconn1lem5  36074  btwnconn1lem13  36082  btwnconn3  36086  segletr  36097  segleantisym  36098  outsideofeq  36113  outsidele  36115  lineunray  36130  refssfne  36341  neibastop2lem  36343  neibastop2  36344  weiunpo  36448  unblimceq0lem  36489  knoppndvlem22  36516  mblfinlem3  37648  mblfinlem4  37649  cnambfre  37657  itg2addnclem  37660  areacirclem5  37701  istotbnd3  37760  crngm4  37992  cvlcvr1  39327  4atlem12  39601  cdlemb  39783  paddasslem10  39818  paddasslem12  39820  paddasslem13  39821  lhpexle3lem  40000  cdlemd4  40190  cdlemefs32sn1aw  40403  cdleme43fsv1snlem  40409  cdleme32d  40433  cdleme32f  40435  cdleme40m  40456  cdleme40n  40457  cdleme50trn2  40540  cdlemftr3  40554  cdlemm10N  41107  dihvalcqpre  41224  dihopelvalcpre  41237  dihmeetlem1N  41279  dihglblem5apreN  41280  dihmeetlem4preN  41295  dihjat1lem  41417  mapd0  41654  mapdh9a  41778  nna4b4nsq  42641  mzpmfp  42728  mzpcompact2lem  42732  diophin  42753  pellexlem3  42812  pellex  42816  pell14qrmulcl  42844  jm2.19lem3  42973  jm2.25  42981  jm2.27b  42988  fnwe2lem2  43033  hbtlem2  43106  hbtlem5  43110  gsumws3  44178  gsumws4  44179  mnuprdlem1  44254  mnuprdlem2  44255  mnuprdlem4  44257  fnchoice  45016  stoweidlem53  46044  stoweidlem61  46052  qndenserrnbllem  46285  bgoldbtbnd  47800  cycldlenngric  47918  grtrimap  47937  isubgr3stgrlem6  47960  prsthinc  49443