Theorem simprrr 782

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  prproe  4909  f1prex  7303  fliftfun  7331  fprresex  8333  wfrlem17OLD  8363  nnaordex2  8675  naddssim  8721  mapdom2  9186  domunfican  9358  fofinf1o  9369  finsschain  9396  wemaplem3  9585  oemapvali  9721  iunfictbso  10151  enfin2i  10358  fin1a2s  10451  distrlem4pr  11063  mulcmpblnr  11108  prsrlem1  11109  addsrmo  11110  mulsrmo  11111  divdivdiv  11965  divsubdiv  11980  lediv12a  12158  xralrple  13243  seqcaopr  14076  leexp2r  14210  hashbclem  14487  wrd2ind  14757  cshwidxmod  14837  rtrclreclem4  15096  relexpindlem  15098  rtrclind  15100  rlimresb  15597  summo  15749  fsum2dlem  15802  prodmo  15968  fprod2dlem  16012  bezoutlem3  16574  bezoutlem4  16575  qredeu  16691  coprmproddvdslem  16695  prmdvdsncoprmbd  16760  pcqmul  16886  pcadd  16922  pockthg  16939  ramub1lem2  17060  cshwsdisj  17132  mreexexlem4d  17691  issubc3  17899  cofucl  17938  setcmon  18140  setcepi  18141  drsdirfi  18362  poslubmo  18468  posglbmo  18469  grprida  18700  ghmpreima  19268  gaorber  19338  psgnunilem4  19529  psgneu  19538  odcau  19636  pgpssslw  19646  fislw  19657  lsmsubm  19685  efgsfo  19771  pgpfac1  20114  pgpfaclem2  20116  pgpfaclem3  20117  unitgrp  20399  islmodd  20880  lmodprop2d  20938  lsspropd  21033  lbsextlem4  21180  assapropd  21909  evlslem1  22123  mdetunilem8  22640  mdetmul  22644  ppttop  23029  epttop  23031  restbas  23181  iscnp4  23286  cnpco  23290  nrmsep  23380  regsep2  23399  ordthauslem  23406  1stcfb  23468  2ndcctbss  23478  2ndcdisj  23479  2ndcomap  23481  dis2ndc  23483  1stcelcls  23484  nlly2i  23499  islly2  23507  hausllycmp  23517  lly1stc  23519  comppfsc  23555  1stckgenlem  23576  ptbasin  23600  txcls  23627  ptcnp  23645  txlly  23659  txnlly  23660  txtube  23663  txcmplem1  23664  txcmplem2  23665  xkococnlem  23682  basqtop  23734  regr1lem  23762  kqreglem1  23764  kqreglem2  23765  kqnrmlem1  23766  kqnrmlem2  23767  reghmph  23816  nrmhmph  23817  filuni  23908  rnelfmlem  23975  fmufil  23982  fclscf  24048  fclsfnflim  24050  flimfnfcls  24051  uffclsflim  24054  cnpfcfi  24063  cnpfcf  24064  alexsublem  24067  alexsubALTlem3  24072  tgpconncompeqg  24135  ghmcnp  24138  qustgplem  24144  blssps  24449  blss  24450  blcld  24533  metequiv2  24538  met2ndci  24550  prdsxmslem2  24557  txmetcnp  24575  nlmvscnlem1  24722  xrge0tsms  24869  ipcnlem1  25292  iscmet3  25340  metsscmetcld  25362  minveclem3  25476  pmltpc  25498  ovolscalem2  25562  ovolicc2lem5  25569  ovolicc2  25570  nulmbl2  25584  ioombl1  25610  uniioombllem6  25636  uniioombl  25637  vitalilem3  25658  i1faddlem  25741  mbfmullem  25774  itg2const2  25790  itg2split  25798  lhop2  26068  dvfsumrlim  26086  itgsubst  26104  plydivex  26353  plyexmo  26369  ulmbdd  26455  cxploglim  27035  dchrptlem2  27323  lgsquad2lem2  27443  2sqlem5  27480  dchrvmasumif  27561  rpvmasum2  27570  dchrisum0re  27571  dchrisum0lem3  27577  dchrisum0  27578  dchrmusum  27582  dchrvmasum  27583  pntibndlem3  27650  pntlemp  27668  ostth3  27696  nosupbday  27764  nosupbnd1lem1  27767  nosupbnd2  27775  noinfbday  27779  noinfbnd1lem1  27782  noinfbnd2  27790  conway  27858  madebdaylemlrcut  27951  mulsproplem9  28164  mulsuniflem  28189  uzsind  28405  readdscl  28445  legtrid  28613  hlcgreu  28640  mirreu3  28676  opphllem  28757  oppperpex  28775  lnperpex  28825  trgcopy  28826  iscgra1  28832  cgraswap  28842  cgracom  28844  cgratr  28845  flatcgra  28846  acopyeu  28856  ax5seglem9  28966  ax5seg  28967  axcontlem8  29000  axcontlem12  29004  upgrclwlkcompim  29813  wwlksnextwrd  29926  2pthfrgr  30312  frgrnbnb  30321  ablo4  30578  smcnlem  30725  pjhthmo  31330  1stpreimas  32720  xrge0tsmsd  33047  locfinref  33801  xpinpreima2  33867  qqhval2  33944  dya2iocnrect  34262  orvcgteel  34448  orvclteel  34453  cnpconn  35214  txpconn  35216  connpconn  35219  pconnpi1  35221  iccllysconn  35234  rellysconn  35235  cvmcov2  35259  cvmliftmolem2  35266  cvmliftmo  35268  cvmliftlem15  35282  cvmliftpht  35302  cvmlift3lem2  35304  cgrextend  35989  btwnouttr2  36003  btwnexch2  36004  cgrxfr  36036  lineext  36057  btwnconn1lem5  36072  btwnconn1lem13  36080  btwnconn3  36084  segletr  36095  segleantisym  36096  outsideofeq  36111  outsidele  36113  lineunray  36128  refssfne  36340  neibastop2lem  36342  neibastop2  36343  weiunpo  36447  unblimceq0lem  36488  knoppndvlem22  36515  mblfinlem3  37645  mblfinlem4  37646  cnambfre  37654  itg2addnclem  37657  areacirclem5  37698  istotbnd3  37757  crngm4  37989  cvlcvr1  39320  4atlem12  39594  cdlemb  39776  paddasslem10  39811  paddasslem12  39813  paddasslem13  39814  lhpexle3lem  39993  cdlemd4  40183  cdlemefs32sn1aw  40396  cdleme43fsv1snlem  40402  cdleme32d  40426  cdleme32f  40428  cdleme40m  40449  cdleme40n  40450  cdleme50trn2  40533  cdlemftr3  40547  cdlemm10N  41100  dihvalcqpre  41217  dihopelvalcpre  41230  dihmeetlem1N  41272  dihglblem5apreN  41273  dihmeetlem4preN  41288  dihjat1lem  41410  mapd0  41647  mapdh9a  41771  nna4b4nsq  42646  mzpmfp  42734  mzpcompact2lem  42738  diophin  42759  pellexlem3  42818  pellex  42822  pell14qrmulcl  42850  jm2.19lem3  42979  jm2.25  42987  jm2.27b  42994  fnwe2lem2  43039  hbtlem2  43112  hbtlem5  43116  gsumws3  44185  gsumws4  44186  mnuprdlem1  44267  mnuprdlem2  44268  mnuprdlem4  44270  fnchoice  44966  stoweidlem53  46008  stoweidlem61  46016  qndenserrnbllem  46249  bgoldbtbnd  47733  grtrimap  47850  isubgr3stgrlem6  47873  prsthinc  48854