Theorem simprrr 779

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  prproe  4846  f1prex  7193  fliftfun  7220  fprresex  8171  wfrlem17OLD  8201  mapdom2  8988  domunfican  9155  fofinf1o  9162  finsschain  9194  wemaplem3  9375  oemapvali  9510  iunfictbso  9940  enfin2i  10147  fin1a2s  10240  distrlem4pr  10852  mulcmpblnr  10897  prsrlem1  10898  addsrmo  10899  mulsrmo  10900  divdivdiv  11746  divsubdiv  11761  lediv12a  11938  xralrple  13009  seqcaopr  13830  leexp2r  13962  hashbclem  14233  wrd2ind  14505  cshwidxmod  14585  rtrclreclem4  14841  relexpindlem  14843  rtrclind  14845  rlimresb  15343  summo  15498  fsum2dlem  15551  prodmo  15715  fprod2dlem  15759  bezoutlem3  16318  bezoutlem4  16319  qredeu  16430  coprmproddvdslem  16434  prmdvdsncoprmbd  16498  pcqmul  16621  pcadd  16657  pockthg  16674  ramub1lem2  16795  cshwsdisj  16867  mreexexlem4d  17423  issubc3  17631  cofucl  17670  setcmon  17869  setcepi  17870  drsdirfi  18090  poslubmo  18196  posglbmo  18197  grpridd  18426  ghmpreima  18923  gaorber  18981  psgnunilem4  19172  psgneu  19181  odcau  19276  pgpssslw  19286  fislw  19297  lsmsubm  19325  efgsfo  19412  pgpfac1  19750  pgpfaclem2  19752  pgpfaclem3  19753  unitgrp  19976  islmodd  20200  lmodprop2d  20256  lsspropd  20350  lbsextlem4  20494  assapropd  21147  evlslem1  21363  mdetunilem8  21839  mdetmul  21843  ppttop  22228  epttop  22230  restbas  22380  iscnp4  22485  cnpco  22489  nrmsep  22579  regsep2  22598  ordthauslem  22605  1stcfb  22667  2ndcctbss  22677  2ndcdisj  22678  2ndcomap  22680  dis2ndc  22682  1stcelcls  22683  nlly2i  22698  islly2  22706  hausllycmp  22716  lly1stc  22718  comppfsc  22754  1stckgenlem  22775  ptbasin  22799  txcls  22826  ptcnp  22844  txlly  22858  txnlly  22859  txtube  22862  txcmplem1  22863  txcmplem2  22864  xkococnlem  22881  basqtop  22933  regr1lem  22961  kqreglem1  22963  kqreglem2  22964  kqnrmlem1  22965  kqnrmlem2  22966  reghmph  23015  nrmhmph  23016  filuni  23107  rnelfmlem  23174  fmufil  23181  fclscf  23247  fclsfnflim  23249  flimfnfcls  23250  uffclsflim  23253  cnpfcfi  23262  cnpfcf  23263  alexsublem  23266  alexsubALTlem3  23271  tgpconncompeqg  23334  ghmcnp  23337  qustgplem  23343  blssps  23648  blss  23649  blcld  23732  metequiv2  23737  met2ndci  23749  prdsxmslem2  23756  txmetcnp  23774  nlmvscnlem1  23921  xrge0tsms  24068  ipcnlem1  24480  iscmet3  24528  metsscmetcld  24550  minveclem3  24664  pmltpc  24685  ovolscalem2  24749  ovolicc2lem5  24756  ovolicc2  24757  nulmbl2  24771  ioombl1  24797  uniioombllem6  24823  uniioombl  24824  vitalilem3  24845  i1faddlem  24928  mbfmullem  24961  itg2const2  24977  itg2split  24985  lhop2  25250  dvfsumrlim  25266  itgsubst  25284  plydivex  25528  plyexmo  25544  ulmbdd  25628  cxploglim  26198  dchrptlem2  26484  lgsquad2lem2  26604  2sqlem5  26641  dchrvmasumif  26722  rpvmasum2  26731  dchrisum0re  26732  dchrisum0lem3  26738  dchrisum0  26739  dchrmusum  26743  dchrvmasum  26744  pntibndlem3  26811  pntlemp  26829  ostth3  26857  legtrid  27060  hlcgreu  27087  mirreu3  27123  opphllem  27204  oppperpex  27222  lnperpex  27272  trgcopy  27273  iscgra1  27279  cgraswap  27289  cgracom  27291  cgratr  27292  flatcgra  27293  acopyeu  27303  ax5seglem9  27413  ax5seg  27414  axcontlem8  27447  axcontlem12  27451  upgrclwlkcompim  28257  wwlksnextwrd  28370  2pthfrgr  28756  frgrnbnb  28765  ablo4  29020  smcnlem  29167  pjhthmo  29772  1stpreimas  31146  xrge0tsmsd  31425  locfinref  31897  xpinpreima2  31963  qqhval2  32038  dya2iocnrect  32354  orvcgteel  32540  orvclteel  32545  cnpconn  33298  txpconn  33300  connpconn  33303  pconnpi1  33305  iccllysconn  33318  rellysconn  33319  cvmcov2  33343  cvmliftmolem2  33350  cvmliftmo  33352  cvmliftlem15  33366  cvmliftpht  33386  cvmlift3lem2  33388  naddssim  33935  nosupbday  33969  nosupbnd1lem1  33972  nosupbnd2  33980  noinfbday  33984  noinfbnd1lem1  33987  noinfbnd2  33995  conway  34054  madebdaylemlrcut  34140  cgrextend  34371  btwnouttr2  34385  btwnexch2  34386  cgrxfr  34418  lineext  34439  btwnconn1lem5  34454  btwnconn1lem13  34462  btwnconn3  34466  segletr  34477  segleantisym  34478  outsideofeq  34493  outsidele  34495  lineunray  34510  refssfne  34608  neibastop2lem  34610  neibastop2  34611  unblimceq0lem  34747  knoppndvlem22  34774  mblfinlem3  35876  mblfinlem4  35877  cnambfre  35885  itg2addnclem  35888  areacirclem5  35929  istotbnd3  35989  crngm4  36221  cvlcvr1  37565  4atlem12  37838  cdlemb  38020  paddasslem10  38055  paddasslem12  38057  paddasslem13  38058  lhpexle3lem  38237  cdlemd4  38427  cdlemefs32sn1aw  38640  cdleme43fsv1snlem  38646  cdleme32d  38670  cdleme32f  38672  cdleme40m  38693  cdleme40n  38694  cdleme50trn2  38777  cdlemftr3  38791  cdlemm10N  39344  dihvalcqpre  39461  dihopelvalcpre  39474  dihmeetlem1N  39516  dihglblem5apreN  39517  dihmeetlem4preN  39532  dihjat1lem  39654  mapd0  39891  mapdh9a  40015  nna4b4nsq  40707  mzpmfp  40779  mzpcompact2lem  40783  diophin  40804  pellexlem3  40863  pellex  40867  pell14qrmulcl  40895  jm2.19lem3  41024  jm2.25  41032  jm2.27b  41039  fnwe2lem2  41087  hbtlem2  41160  hbtlem5  41164  gsumws3  42035  gsumws4  42036  mnuprdlem1  42118  mnuprdlem2  42119  mnuprdlem4  42121  fnchoice  42800  stoweidlem53  43838  stoweidlem61  43846  qndenserrnbllem  44079  bgoldbtbnd  45520  prsthinc  46594