Theorem simprrr 772

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

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  prproe  4669  f1prex  6811  fliftfun  6834  grpridd  7151  wfrlem17  7714  mapdom2  8419  domunfican  8521  fofinf1o  8529  finsschain  8561  wemaplem3  8742  oemapvali  8878  iunfictbso  9270  enfin2i  9478  fin1a2s  9571  distrlem4pr  10183  mulcmpblnr  10228  prsrlem1  10229  addsrmo  10230  mulsrmo  10231  divdivdiv  11076  divsubdiv  11091  lediv12a  11270  xralrple  12348  seqcaopr  13156  leexp2r  13236  hashbclem  13550  wrd2ind  13844  wrd2indOLD  13845  cshwidxmod  13954  rtrclreclem4  14208  relexpindlem  14210  rtrclind  14212  rlimresb  14704  summo  14855  fsum2dlem  14906  prodmo  15069  fprod2dlem  15113  bezoutlem3  15664  bezoutlem4  15665  qredeu  15777  coprmproddvdslem  15781  pcqmul  15962  pcadd  15997  pockthg  16014  ramub1lem2  16135  cshwsdisj  16204  mreexexlem4d  16693  issubc3  16894  cofucl  16933  setcmon  17122  setcepi  17123  drsdirfi  17324  poslubmo  17532  posglbmo  17533  ghmpreima  18066  gaorber  18124  psgnunilem4  18301  psgneu  18310  odcau  18403  pgpssslw  18413  fislw  18424  lsmsubm  18452  efgsfo  18537  pgpfac1  18866  pgpfaclem2  18868  pgpfaclem3  18869  unitgrp  19054  islmodd  19261  lmodprop2d  19317  lsspropd  19412  lbsextlem4  19558  assapropd  19724  evlslem1  19911  mdetunilem8  20830  mdetmul  20834  ppttop  21219  epttop  21221  restbas  21370  iscnp4  21475  cnpco  21479  nrmsep  21569  regsep2  21588  ordthauslem  21595  1stcfb  21657  2ndcctbss  21667  2ndcdisj  21668  2ndcomap  21670  dis2ndc  21672  1stcelcls  21673  nlly2i  21688  islly2  21696  hausllycmp  21706  lly1stc  21708  comppfsc  21744  1stckgenlem  21765  ptbasin  21789  txcls  21816  ptcnp  21834  txlly  21848  txnlly  21849  txtube  21852  txcmplem1  21853  txcmplem2  21854  xkococnlem  21871  basqtop  21923  regr1lem  21951  kqreglem1  21953  kqreglem2  21954  kqnrmlem1  21955  kqnrmlem2  21956  reghmph  22005  nrmhmph  22006  filuni  22097  rnelfmlem  22164  fmufil  22171  fclscf  22237  fclsfnflim  22239  flimfnfcls  22240  uffclsflim  22243  cnpfcfi  22252  cnpfcf  22253  alexsublem  22256  alexsubALTlem3  22261  tgpconncompeqg  22323  ghmcnp  22326  qustgplem  22332  blssps  22637  blss  22638  blcld  22718  metequiv2  22723  met2ndci  22735  prdsxmslem2  22742  txmetcnp  22760  nlmvscnlem1  22898  xrge0tsms  23045  ipcnlem1  23451  iscmet3  23499  metsscmetcld  23521  minveclem3  23635  pmltpc  23654  ovolscalem2  23718  ovolicc2lem5  23725  ovolicc2  23726  nulmbl2  23740  ioombl1  23766  uniioombllem6  23792  uniioombl  23793  vitalilem3  23814  i1faddlem  23897  mbfmullem  23929  itg2const2  23945  itg2split  23953  lhop2  24215  dvfsumrlim  24231  itgsubst  24249  plydivex  24489  plyexmo  24505  ulmbdd  24589  cxploglim  25156  dchrptlem2  25442  lgsquad2lem2  25562  2sqlem5  25599  dchrvmasumif  25644  rpvmasum2  25653  dchrisum0re  25654  dchrisum0lem3  25660  dchrisum0  25661  dchrmusum  25665  dchrvmasum  25666  pntibndlem3  25733  pntlemp  25751  ostth3  25779  legtrid  25942  hlcgreu  25969  mirreu3  26005  opphllem  26083  oppperpex  26101  lnperpex  26151  trgcopy  26152  iscgra1  26158  cgraswap  26168  cgracom  26170  cgratr  26171  flatcgra  26172  acopyeu  26183  ax5seglem9  26286  ax5seg  26287  axcontlem8  26320  axcontlem12  26324  upgrclwlkcompim  27133  wlkwwlkfunOLD  27246  wwlksnextwrd  27261  wwlksnextwrdOLD  27266  2pthfrgr  27692  frgrnbnb  27701  ablo4  27977  smcnlem  28124  pjhthmo  28733  1stpreimas  30049  xrge0tsmsd  30347  locfinref  30506  xpinpreima2  30551  qqhval2  30624  dya2iocnrect  30941  orvcgteel  31128  orvclteel  31133  cnpconn  31811  txpconn  31813  connpconn  31816  pconnpi1  31818  iccllysconn  31831  rellysconn  31832  cvmcov2  31856  cvmliftmolem2  31863  cvmliftmo  31865  cvmliftlem15  31879  cvmliftpht  31899  cvmlift3lem2  31901  nosupbnd1lem1  32443  nosupbnd2  32451  conway  32499  cgrextend  32704  btwnouttr2  32718  btwnexch2  32719  cgrxfr  32751  lineext  32772  btwnconn1lem5  32787  btwnconn1lem13  32795  btwnconn3  32799  segletr  32810  segleantisym  32811  outsideofeq  32826  outsidele  32828  lineunray  32843  refssfne  32941  neibastop2lem  32943  neibastop2  32944  unblimceq0lem  33079  knoppndvlem22  33106  mblfinlem3  34074  mblfinlem4  34075  cnambfre  34083  itg2addnclem  34086  areacirclem5  34129  istotbnd3  34194  crngm4  34426  cvlcvr1  35493  4atlem12  35766  cdlemb  35948  paddasslem10  35983  paddasslem12  35985  paddasslem13  35986  lhpexle3lem  36165  cdlemd4  36355  cdlemefs32sn1aw  36568  cdleme43fsv1snlem  36574  cdleme32d  36598  cdleme32f  36600  cdleme40m  36621  cdleme40n  36622  cdleme50trn2  36705  cdlemftr3  36719  cdlemm10N  37272  dihvalcqpre  37389  dihopelvalcpre  37402  dihmeetlem1N  37444  dihglblem5apreN  37445  dihmeetlem4preN  37460  dihjat1lem  37582  mapd0  37819  mapdh9a  37943  mzpmfp  38270  mzpcompact2lem  38274  diophin  38296  pellexlem3  38355  pellex  38359  pell14qrmulcl  38387  jm2.19lem3  38517  jm2.25  38525  jm2.27b  38532  fnwe2lem2  38580  hbtlem2  38653  hbtlem5  38657  gsumws3  39455  gsumws4  39456  fnchoice  40121  stoweidlem53  41197  stoweidlem61  41205  qndenserrnbllem  41438  bgoldbtbnd  42722