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

Syntax hints:   → wi 4   ∧ wa 398

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 399

This theorem is referenced by:  prproe  4835  f1prex  7039  fliftfun  7064  wfrlem17  7970  mapdom2  8687  domunfican  8790  fofinf1o  8798  finsschain  8830  wemaplem3  9011  oemapvali  9146  iunfictbso  9539  enfin2i  9742  fin1a2s  9835  distrlem4pr  10447  mulcmpblnr  10492  prsrlem1  10493  addsrmo  10494  mulsrmo  10495  divdivdiv  11340  divsubdiv  11355  lediv12a  11532  xralrple  12597  seqcaopr  13406  leexp2r  13537  hashbclem  13809  wrd2ind  14084  cshwidxmod  14164  rtrclreclem4  14419  relexpindlem  14421  rtrclind  14423  rlimresb  14921  summo  15073  fsum2dlem  15124  prodmo  15289  fprod2dlem  15333  bezoutlem3  15888  bezoutlem4  15889  qredeu  16001  coprmproddvdslem  16005  pcqmul  16189  pcadd  16224  pockthg  16241  ramub1lem2  16362  cshwsdisj  16431  mreexexlem4d  16917  issubc3  17118  cofucl  17157  setcmon  17346  setcepi  17347  drsdirfi  17547  poslubmo  17755  posglbmo  17756  grpridd  17884  ghmpreima  18379  gaorber  18437  psgnunilem4  18624  psgneu  18633  odcau  18728  pgpssslw  18738  fislw  18749  lsmsubm  18777  efgsfo  18864  pgpfac1  19201  pgpfaclem2  19203  pgpfaclem3  19204  unitgrp  19416  islmodd  19639  lmodprop2d  19695  lsspropd  19788  lbsextlem4  19932  assapropd  20100  evlslem1  20294  mdetunilem8  21227  mdetmul  21231  ppttop  21614  epttop  21616  restbas  21765  iscnp4  21870  cnpco  21874  nrmsep  21964  regsep2  21983  ordthauslem  21990  1stcfb  22052  2ndcctbss  22062  2ndcdisj  22063  2ndcomap  22065  dis2ndc  22067  1stcelcls  22068  nlly2i  22083  islly2  22091  hausllycmp  22101  lly1stc  22103  comppfsc  22139  1stckgenlem  22160  ptbasin  22184  txcls  22211  ptcnp  22229  txlly  22243  txnlly  22244  txtube  22247  txcmplem1  22248  txcmplem2  22249  xkococnlem  22266  basqtop  22318  regr1lem  22346  kqreglem1  22348  kqreglem2  22349  kqnrmlem1  22350  kqnrmlem2  22351  reghmph  22400  nrmhmph  22401  filuni  22492  rnelfmlem  22559  fmufil  22566  fclscf  22632  fclsfnflim  22634  flimfnfcls  22635  uffclsflim  22638  cnpfcfi  22647  cnpfcf  22648  alexsublem  22651  alexsubALTlem3  22656  tgpconncompeqg  22719  ghmcnp  22722  qustgplem  22728  blssps  23033  blss  23034  blcld  23114  metequiv2  23119  met2ndci  23131  prdsxmslem2  23138  txmetcnp  23156  nlmvscnlem1  23294  xrge0tsms  23441  ipcnlem1  23847  iscmet3  23895  metsscmetcld  23917  minveclem3  24031  pmltpc  24050  ovolscalem2  24114  ovolicc2lem5  24121  ovolicc2  24122  nulmbl2  24136  ioombl1  24162  uniioombllem6  24188  uniioombl  24189  vitalilem3  24210  i1faddlem  24293  mbfmullem  24325  itg2const2  24341  itg2split  24349  lhop2  24611  dvfsumrlim  24627  itgsubst  24645  plydivex  24885  plyexmo  24901  ulmbdd  24985  cxploglim  25554  dchrptlem2  25840  lgsquad2lem2  25960  2sqlem5  25997  dchrvmasumif  26078  rpvmasum2  26087  dchrisum0re  26088  dchrisum0lem3  26094  dchrisum0  26095  dchrmusum  26099  dchrvmasum  26100  pntibndlem3  26167  pntlemp  26185  ostth3  26213  legtrid  26376  hlcgreu  26403  mirreu3  26439  opphllem  26520  oppperpex  26538  lnperpex  26588  trgcopy  26589  iscgra1  26595  cgraswap  26605  cgracom  26607  cgratr  26608  flatcgra  26609  acopyeu  26619  ax5seglem9  26722  ax5seg  26723  axcontlem8  26756  axcontlem12  26760  upgrclwlkcompim  27561  wwlksnextwrd  27674  2pthfrgr  28062  frgrnbnb  28071  ablo4  28326  smcnlem  28473  pjhthmo  29078  1stpreimas  30440  xrge0tsmsd  30692  locfinref  31105  xpinpreima2  31150  qqhval2  31223  dya2iocnrect  31539  orvcgteel  31725  orvclteel  31730  cnpconn  32477  txpconn  32479  connpconn  32482  pconnpi1  32484  iccllysconn  32497  rellysconn  32498  cvmcov2  32522  cvmliftmolem2  32529  cvmliftmo  32531  cvmliftlem15  32545  cvmliftpht  32565  cvmlift3lem2  32567  nosupbnd1lem1  33208  nosupbnd2  33216  conway  33264  cgrextend  33469  btwnouttr2  33483  btwnexch2  33484  cgrxfr  33516  lineext  33537  btwnconn1lem5  33552  btwnconn1lem13  33560  btwnconn3  33564  segletr  33575  segleantisym  33576  outsideofeq  33591  outsidele  33593  lineunray  33608  refssfne  33706  neibastop2lem  33708  neibastop2  33709  unblimceq0lem  33845  knoppndvlem22  33872  mblfinlem3  34930  mblfinlem4  34931  cnambfre  34939  itg2addnclem  34942  areacirclem5  34985  istotbnd3  35048  crngm4  35280  cvlcvr1  36474  4atlem12  36747  cdlemb  36929  paddasslem10  36964  paddasslem12  36966  paddasslem13  36967  lhpexle3lem  37146  cdlemd4  37336  cdlemefs32sn1aw  37549  cdleme43fsv1snlem  37555  cdleme32d  37579  cdleme32f  37581  cdleme40m  37602  cdleme40n  37603  cdleme50trn2  37686  cdlemftr3  37700  cdlemm10N  38253  dihvalcqpre  38370  dihopelvalcpre  38383  dihmeetlem1N  38425  dihglblem5apreN  38426  dihmeetlem4preN  38441  dihjat1lem  38563  mapd0  38800  mapdh9a  38924  mzpmfp  39342  mzpcompact2lem  39346  diophin  39367  pellexlem3  39426  pellex  39430  pell14qrmulcl  39458  jm2.19lem3  39586  jm2.25  39594  jm2.27b  39601  fnwe2lem2  39649  hbtlem2  39722  hbtlem5  39726  gsumws3  40547  gsumws4  40548  mnuprdlem1  40606  mnuprdlem2  40607  mnuprdlem4  40609  fnchoice  41284  stoweidlem53  42337  stoweidlem61  42345  qndenserrnbllem  42578  bgoldbtbnd  43973