Theorem simprrr 791

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 488	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜃)
2	1	ad2antll 739	1 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜃)

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 209  df-an 400

This theorem is referenced by:  prproe  4864  f1prex  7268  fliftfun  7296  fprresex  8291  nnaordex2  8609  naddssim  8656  mapdom2  9120  domunfican  9265  fofinf1o  9273  finsschain  9300  wemaplem3  9494  oemapvali  9637  iunfictbso  10082  enfin2i  10289  fin1a2s  10382  distrlem4pr  10995  mulcmpblnr  11040  prsrlem1  11041  addsrmo  11042  mulsrmo  11043  divdivdiv  11903  divsubdiv  11918  lediv12a  12095  xralrple  13218  seqcaopr  14062  leexp2r  14197  hashbclem  14475  wrd2ind  14746  cshwidxmod  14826  rtrclreclem4  15084  relexpindlem  15086  rtrclind  15088  rlimresb  15602  summo  15754  fsum2dlem  15807  prodmo  15976  fprod2dlem  16020  bezoutlem3  16585  bezoutlem4  16586  qredeu  16702  coprmproddvdslem  16706  prmdvdsncoprmbd  16772  pcqmul  16899  pcadd  16935  pockthg  16952  ramub1lem2  17073  cshwsdisj  17144  mreexexlem4d  17689  issubc3  17892  cofucl  17931  setcmon  18130  setcepi  18131  drsdirfi  18347  poslubmo  18451  posglbmo  18452  grprida  18719  ghmpreima  19288  gaorber  19358  psgnunilem4  19547  psgneu  19556  odcau  19654  pgpssslw  19664  fislw  19675  lsmsubm  19703  efgsfo  19789  pgpfac1  20132  pgpfaclem2  20134  pgpfaclem3  20135  unitgrp  20442  islmodd  20940  lmodprop2d  20998  lsspropd  21091  lbsextlem4  21238  assapropd  21930  evlslem1  22142  mdetunilem8  22686  mdetmul  22690  ppttop  23074  epttop  23076  restbas  23225  iscnp4  23330  cnpco  23334  nrmsep  23424  regsep2  23443  ordthauslem  23450  1stcfb  23512  2ndcctbss  23522  2ndcdisj  23523  2ndcomap  23525  dis2ndc  23527  1stcelcls  23528  nlly2i  23543  islly2  23551  hausllycmp  23561  lly1stc  23563  comppfsc  23599  1stckgenlem  23620  ptbasin  23644  txcls  23671  ptcnp  23689  txlly  23703  txnlly  23704  txtube  23707  txcmplem1  23708  txcmplem2  23709  xkococnlem  23726  basqtop  23778  regr1lem  23806  kqreglem1  23808  kqreglem2  23809  kqnrmlem1  23810  kqnrmlem2  23811  reghmph  23860  nrmhmph  23861  filuni  23952  rnelfmlem  24019  fmufil  24026  fclscf  24092  fclsfnflim  24094  flimfnfcls  24095  uffclsflim  24098  cnpfcfi  24107  cnpfcf  24108  alexsublem  24111  alexsubALTlem3  24116  tgpconncompeqg  24179  ghmcnp  24182  qustgplem  24188  blssps  24491  blss  24492  blcld  24572  metequiv2  24577  met2ndci  24589  prdsxmslem2  24596  txmetcnp  24614  nlmvscnlem1  24753  xrge0tsms  24902  ipcnlem1  25314  iscmet3  25362  metsscmetcld  25384  minveclem3  25498  pmltpc  25519  ovolscalem2  25583  ovolicc2lem5  25590  ovolicc2  25591  nulmbl2  25605  ioombl1  25631  uniioombllem6  25657  uniioombl  25658  vitalilem3  25679  i1faddlem  25762  mbfmullem  25794  itg2const2  25810  itg2split  25818  lhop2  26084  dvfsumrlim  26100  itgsubst  26118  plydivex  26368  plyexmo  26384  ulmbdd  26468  cxploglim  27049  dchrptlem2  27336  lgsquad2lem2  27456  2sqlem5  27493  dchrvmasumif  27574  rpvmasum2  27583  dchrisum0re  27584  dchrisum0lem3  27590  dchrisum0  27591  dchrmusum  27595  dchrvmasum  27596  pntibndlem3  27663  pntlemp  27681  ostth3  27709  nosupbday  27776  nosupbnd1lem1  27779  nosupbnd2  27787  noinfbday  27791  noinfbnd1lem1  27794  noinfbnd2  27802  conway  27879  madebdaylemlrcut  27999  mulsproplem9  28224  mulsuniflem  28249  uzsind  28505  bdayfinbndlem1  28567  readdscl  28599  legtrid  28767  hlcgreu  28794  mirreu3  28834  opphllem  28915  oppperpex  28933  lnperpex  28983  trgcopy  28984  iscgra1  29011  cgraswap  29021  cgracom  29023  cgratr  29024  flatcgra  29025  acopyeu  29035  ax5seglem9  29145  ax5seg  29146  axcontlem8  29179  axcontlem12  29183  upgrclwlkcompim  29988  wwlksnextwrd  30104  2pthfrgr  30493  frgrnbnb  30502  ablo4  30760  smcnlem  30907  pjhthmo  31512  1stpreimas  32914  xrge0tsmsd  33259  locfinref  34140  xpinpreima2  34206  qqhval2  34281  dya2iocnrect  34580  orvcgteel  34767  orvclteel  34772  cnpconn  35585  txpconn  35587  connpconn  35590  pconnpi1  35592  iccllysconn  35605  rellysconn  35606  cvmcov2  35630  cvmliftmolem2  35637  cvmliftmo  35639  cvmliftlem15  35653  cvmliftpht  35673  cvmlift3lem2  35675  cgrextend  36363  btwnouttr2  36377  btwnexch2  36378  cgrxfr  36410  lineext  36431  btwnconn1lem5  36446  btwnconn1lem13  36454  btwnconn3  36458  segletr  36469  segleantisym  36470  outsideofeq  36485  outsidele  36487  lineunray  36502  refssfne  36723  neibastop2lem  36725  neibastop2  36726  weiunpo  36830  unblimceq0lem  36949  knoppndvlem22  36976  mblfinlem3  38163  mblfinlem4  38164  cnambfre  38172  itg2addnclem  38175  areacirclem5  38216  istotbnd3  38275  crngm4  38507  cvlcvr1  39968  4atlem12  40241  cdlemb  40423  paddasslem10  40458  paddasslem12  40460  paddasslem13  40461  lhpexle3lem  40640  cdlemd4  40830  cdlemefs32sn1aw  41043  cdleme43fsv1snlem  41049  cdleme32d  41073  cdleme32f  41075  cdleme40m  41096  cdleme40n  41097  cdleme50trn2  41180  cdlemftr3  41194  cdlemm10N  41747  dihvalcqpre  41864  dihopelvalcpre  41877  dihmeetlem1N  41919  dihglblem5apreN  41920  dihmeetlem4preN  41935  dihjat1lem  42057  mapd0  42294  mapdh9a  42418  nna4b4nsq  43247  mzpmfp  43333  mzpcompact2lem  43337  diophin  43358  pellexlem3  43413  pellex  43417  pell14qrmulcl  43445  jm2.19lem3  43573  jm2.25  43581  jm2.27b  43588  fnwe2lem2  43633  hbtlem2  43706  hbtlem5  43710  gsumws3  44777  gsumws4  44778  mnuprdlem1  44839  mnuprdlem2  44840  mnuprdlem4  44842  fnchoice  45600  stoweidlem53  46618  stoweidlem61  46626  qndenserrnbllem  46859  bgoldbtbnd  48422  cycldlenngric  48541  grtrimap  48561  isubgr3stgrlem6  48584  prsthinc  50076