Theorem simprrr 780

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  prproe  4906  f1prex  7291  fliftfun  7317  fprresex  8314  wfrlem17OLD  8344  nnaordex2  8658  naddssim  8704  mapdom2  9171  domunfican  9344  fofinf1o  9351  finsschain  9383  wemaplem3  9571  oemapvali  9707  iunfictbso  10137  enfin2i  10344  fin1a2s  10437  distrlem4pr  11049  mulcmpblnr  11094  prsrlem1  11095  addsrmo  11096  mulsrmo  11097  divdivdiv  11945  divsubdiv  11960  lediv12a  12137  xralrple  13216  seqcaopr  14036  leexp2r  14170  hashbclem  14443  wrd2ind  14705  cshwidxmod  14785  rtrclreclem4  15040  relexpindlem  15042  rtrclind  15044  rlimresb  15541  summo  15695  fsum2dlem  15748  prodmo  15912  fprod2dlem  15956  bezoutlem3  16516  bezoutlem4  16517  qredeu  16628  coprmproddvdslem  16632  prmdvdsncoprmbd  16698  pcqmul  16821  pcadd  16857  pockthg  16874  ramub1lem2  16995  cshwsdisj  17067  mreexexlem4d  17626  issubc3  17834  cofucl  17873  setcmon  18075  setcepi  18076  drsdirfi  18296  poslubmo  18402  posglbmo  18403  grprida  18634  ghmpreima  19196  gaorber  19263  psgnunilem4  19456  psgneu  19465  odcau  19563  pgpssslw  19573  fislw  19584  lsmsubm  19612  efgsfo  19698  pgpfac1  20041  pgpfaclem2  20043  pgpfaclem3  20044  unitgrp  20326  islmodd  20753  lmodprop2d  20811  lsspropd  20906  lbsextlem4  21053  assapropd  21809  evlslem1  22035  mdetunilem8  22551  mdetmul  22555  ppttop  22940  epttop  22942  restbas  23092  iscnp4  23197  cnpco  23201  nrmsep  23291  regsep2  23310  ordthauslem  23317  1stcfb  23379  2ndcctbss  23389  2ndcdisj  23390  2ndcomap  23392  dis2ndc  23394  1stcelcls  23395  nlly2i  23410  islly2  23418  hausllycmp  23428  lly1stc  23430  comppfsc  23466  1stckgenlem  23487  ptbasin  23511  txcls  23538  ptcnp  23556  txlly  23570  txnlly  23571  txtube  23574  txcmplem1  23575  txcmplem2  23576  xkococnlem  23593  basqtop  23645  regr1lem  23673  kqreglem1  23675  kqreglem2  23676  kqnrmlem1  23677  kqnrmlem2  23678  reghmph  23727  nrmhmph  23728  filuni  23819  rnelfmlem  23886  fmufil  23893  fclscf  23959  fclsfnflim  23961  flimfnfcls  23962  uffclsflim  23965  cnpfcfi  23974  cnpfcf  23975  alexsublem  23978  alexsubALTlem3  23983  tgpconncompeqg  24046  ghmcnp  24049  qustgplem  24055  blssps  24360  blss  24361  blcld  24444  metequiv2  24449  met2ndci  24461  prdsxmslem2  24468  txmetcnp  24486  nlmvscnlem1  24633  xrge0tsms  24780  ipcnlem1  25203  iscmet3  25251  metsscmetcld  25273  minveclem3  25387  pmltpc  25409  ovolscalem2  25473  ovolicc2lem5  25480  ovolicc2  25481  nulmbl2  25495  ioombl1  25521  uniioombllem6  25547  uniioombl  25548  vitalilem3  25569  i1faddlem  25652  mbfmullem  25685  itg2const2  25701  itg2split  25709  lhop2  25978  dvfsumrlim  25996  itgsubst  26014  plydivex  26262  plyexmo  26278  ulmbdd  26364  cxploglim  26940  dchrptlem2  27228  lgsquad2lem2  27348  2sqlem5  27385  dchrvmasumif  27466  rpvmasum2  27475  dchrisum0re  27476  dchrisum0lem3  27482  dchrisum0  27483  dchrmusum  27487  dchrvmasum  27488  pntibndlem3  27555  pntlemp  27573  ostth3  27601  nosupbday  27668  nosupbnd1lem1  27671  nosupbnd2  27679  noinfbday  27683  noinfbnd1lem1  27686  noinfbnd2  27694  conway  27762  madebdaylemlrcut  27855  mulsproplem9  28058  mulsuniflem  28083  readdscl  28283  legtrid  28451  hlcgreu  28478  mirreu3  28514  opphllem  28595  oppperpex  28613  lnperpex  28663  trgcopy  28664  iscgra1  28670  cgraswap  28680  cgracom  28682  cgratr  28683  flatcgra  28684  acopyeu  28694  ax5seglem9  28804  ax5seg  28805  axcontlem8  28838  axcontlem12  28842  upgrclwlkcompim  29651  wwlksnextwrd  29764  2pthfrgr  30150  frgrnbnb  30159  ablo4  30416  smcnlem  30563  pjhthmo  31168  1stpreimas  32542  xrge0tsmsd  32828  locfinref  33512  xpinpreima2  33578  qqhval2  33653  dya2iocnrect  33971  orvcgteel  34157  orvclteel  34162  cnpconn  34910  txpconn  34912  connpconn  34915  pconnpi1  34917  iccllysconn  34930  rellysconn  34931  cvmcov2  34955  cvmliftmolem2  34962  cvmliftmo  34964  cvmliftlem15  34978  cvmliftpht  34998  cvmlift3lem2  35000  cgrextend  35674  btwnouttr2  35688  btwnexch2  35689  cgrxfr  35721  lineext  35742  btwnconn1lem5  35757  btwnconn1lem13  35765  btwnconn3  35769  segletr  35780  segleantisym  35781  outsideofeq  35796  outsidele  35798  lineunray  35813  refssfne  35912  neibastop2lem  35914  neibastop2  35915  unblimceq0lem  36051  knoppndvlem22  36078  mblfinlem3  37202  mblfinlem4  37203  cnambfre  37211  itg2addnclem  37214  areacirclem5  37255  istotbnd3  37314  crngm4  37546  cvlcvr1  38880  4atlem12  39154  cdlemb  39336  paddasslem10  39371  paddasslem12  39373  paddasslem13  39374  lhpexle3lem  39553  cdlemd4  39743  cdlemefs32sn1aw  39956  cdleme43fsv1snlem  39962  cdleme32d  39986  cdleme32f  39988  cdleme40m  40009  cdleme40n  40010  cdleme50trn2  40093  cdlemftr3  40107  cdlemm10N  40660  dihvalcqpre  40777  dihopelvalcpre  40790  dihmeetlem1N  40832  dihglblem5apreN  40833  dihmeetlem4preN  40848  dihjat1lem  40970  mapd0  41207  mapdh9a  41331  nna4b4nsq  42149  mzpmfp  42232  mzpcompact2lem  42236  diophin  42257  pellexlem3  42316  pellex  42320  pell14qrmulcl  42348  jm2.19lem3  42477  jm2.25  42485  jm2.27b  42492  fnwe2lem2  42540  hbtlem2  42613  hbtlem5  42617  gsumws3  43691  gsumws4  43692  mnuprdlem1  43774  mnuprdlem2  43775  mnuprdlem4  43777  fnchoice  44456  stoweidlem53  45504  stoweidlem61  45512  qndenserrnbllem  45745  bgoldbtbnd  47212  prsthinc  48172