Theorem simprrr 788

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  prproe  4838  f1prex  7231  fliftfun  7259  fprresex  8253  nnaordex2  8569  naddssim  8615  mapdom2  9080  domunfican  9226  fofinf1o  9236  finsschain  9263  wemaplem3  9457  oemapvali  9600  iunfictbso  10031  enfin2i  10239  fin1a2s  10332  distrlem4pr  10945  mulcmpblnr  10990  prsrlem1  10991  addsrmo  10992  mulsrmo  10993  divdivdiv  11851  divsubdiv  11866  lediv12a  12044  xralrple  13152  seqcaopr  13996  leexp2r  14131  hashbclem  14409  wrd2ind  14680  cshwidxmod  14760  rtrclreclem4  15018  relexpindlem  15020  rtrclind  15022  rlimresb  15522  summo  15674  fsum2dlem  15727  prodmo  15896  fprod2dlem  15940  bezoutlem3  16505  bezoutlem4  16506  qredeu  16622  coprmproddvdslem  16626  prmdvdsncoprmbd  16692  pcqmul  16819  pcadd  16855  pockthg  16872  ramub1lem2  16993  cshwsdisj  17064  mreexexlem4d  17608  issubc3  17811  cofucl  17850  setcmon  18049  setcepi  18050  drsdirfi  18266  poslubmo  18370  posglbmo  18371  grprida  18638  ghmpreima  19207  gaorber  19277  psgnunilem4  19466  psgneu  19475  odcau  19573  pgpssslw  19583  fislw  19594  lsmsubm  19622  efgsfo  19708  pgpfac1  20051  pgpfaclem2  20053  pgpfaclem3  20054  unitgrp  20357  islmodd  20859  lmodprop2d  20917  lsspropd  21010  lbsextlem4  21157  assapropd  21849  evlslem1  22061  mdetunilem8  22605  mdetmul  22609  ppttop  22993  epttop  22995  restbas  23144  iscnp4  23249  cnpco  23253  nrmsep  23343  regsep2  23362  ordthauslem  23369  1stcfb  23431  2ndcctbss  23441  2ndcdisj  23442  2ndcomap  23444  dis2ndc  23446  1stcelcls  23447  nlly2i  23462  islly2  23470  hausllycmp  23480  lly1stc  23482  comppfsc  23518  1stckgenlem  23539  ptbasin  23563  txcls  23590  ptcnp  23608  txlly  23622  txnlly  23623  txtube  23626  txcmplem1  23627  txcmplem2  23628  xkococnlem  23645  basqtop  23697  regr1lem  23725  kqreglem1  23727  kqreglem2  23728  kqnrmlem1  23729  kqnrmlem2  23730  reghmph  23779  nrmhmph  23780  filuni  23871  rnelfmlem  23938  fmufil  23945  fclscf  24011  fclsfnflim  24013  flimfnfcls  24014  uffclsflim  24017  cnpfcfi  24026  cnpfcf  24027  alexsublem  24030  alexsubALTlem3  24035  tgpconncompeqg  24098  ghmcnp  24101  qustgplem  24107  blssps  24410  blss  24411  blcld  24491  metequiv2  24496  met2ndci  24508  prdsxmslem2  24515  txmetcnp  24533  nlmvscnlem1  24672  xrge0tsms  24821  ipcnlem1  25233  iscmet3  25281  metsscmetcld  25303  minveclem3  25417  pmltpc  25438  ovolscalem2  25502  ovolicc2lem5  25509  ovolicc2  25510  nulmbl2  25524  ioombl1  25550  uniioombllem6  25576  uniioombl  25577  vitalilem3  25598  i1faddlem  25681  mbfmullem  25713  itg2const2  25729  itg2split  25737  lhop2  26003  dvfsumrlim  26019  itgsubst  26037  plydivex  26284  plyexmo  26300  ulmbdd  26384  cxploglim  26962  dchrptlem2  27249  lgsquad2lem2  27369  2sqlem5  27406  dchrvmasumif  27487  rpvmasum2  27496  dchrisum0re  27497  dchrisum0lem3  27503  dchrisum0  27504  dchrmusum  27508  dchrvmasum  27509  pntibndlem3  27576  pntlemp  27594  ostth3  27622  nosupbday  27689  nosupbnd1lem1  27692  nosupbnd2  27700  noinfbday  27704  noinfbnd1lem1  27707  noinfbnd2  27715  conway  27791  madebdaylemlrcut  27911  mulsproplem9  28136  mulsuniflem  28161  uzsind  28417  bdayfinbndlem1  28479  readdscl  28511  legtrid  28679  hlcgreu  28706  mirreu3  28742  opphllem  28823  oppperpex  28841  lnperpex  28891  trgcopy  28892  iscgra1  28898  cgraswap  28908  cgracom  28910  cgratr  28911  flatcgra  28912  acopyeu  28922  ax5seglem9  29026  ax5seg  29027  axcontlem8  29060  axcontlem12  29064  upgrclwlkcompim  29869  wwlksnextwrd  29985  2pthfrgr  30374  frgrnbnb  30383  ablo4  30641  smcnlem  30788  pjhthmo  31393  1stpreimas  32800  xrge0tsmsd  33156  locfinref  34035  xpinpreima2  34101  qqhval2  34176  dya2iocnrect  34475  orvcgteel  34662  orvclteel  34667  cnpconn  35471  txpconn  35473  connpconn  35476  pconnpi1  35478  iccllysconn  35491  rellysconn  35492  cvmcov2  35516  cvmliftmolem2  35523  cvmliftmo  35525  cvmliftlem15  35539  cvmliftpht  35559  cvmlift3lem2  35561  cgrextend  36249  btwnouttr2  36263  btwnexch2  36264  cgrxfr  36296  lineext  36317  btwnconn1lem5  36332  btwnconn1lem13  36340  btwnconn3  36344  segletr  36355  segleantisym  36356  outsideofeq  36371  outsidele  36373  lineunray  36388  refssfne  36599  neibastop2lem  36601  neibastop2  36602  weiunpo  36706  unblimceq0lem  36825  knoppndvlem22  36852  mblfinlem3  38039  mblfinlem4  38040  cnambfre  38048  itg2addnclem  38051  areacirclem5  38092  istotbnd3  38151  crngm4  38383  cvlcvr1  39844  4atlem12  40117  cdlemb  40299  paddasslem10  40334  paddasslem12  40336  paddasslem13  40337  lhpexle3lem  40516  cdlemd4  40706  cdlemefs32sn1aw  40919  cdleme43fsv1snlem  40925  cdleme32d  40949  cdleme32f  40951  cdleme40m  40972  cdleme40n  40973  cdleme50trn2  41056  cdlemftr3  41070  cdlemm10N  41623  dihvalcqpre  41740  dihopelvalcpre  41753  dihmeetlem1N  41795  dihglblem5apreN  41796  dihmeetlem4preN  41811  dihjat1lem  41933  mapd0  42170  mapdh9a  42294  nna4b4nsq  43123  mzpmfp  43209  mzpcompact2lem  43213  diophin  43234  pellexlem3  43289  pellex  43293  pell14qrmulcl  43321  jm2.19lem3  43449  jm2.25  43457  jm2.27b  43464  fnwe2lem2  43509  hbtlem2  43582  hbtlem5  43586  gsumws3  44653  gsumws4  44654  mnuprdlem1  44729  mnuprdlem2  44730  mnuprdlem4  44732  fnchoice  45490  stoweidlem53  46508  stoweidlem61  46516  qndenserrnbllem  46749  bgoldbtbnd  48312  cycldlenngric  48431  grtrimap  48451  isubgr3stgrlem6  48474  prsthinc  49966