Theorem simprrr 781

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  4881  f1prex  7276  fliftfun  7304  fprresex  8307  wfrlem17OLD  8337  nnaordex2  8649  naddssim  8695  mapdom2  9160  domunfican  9331  fofinf1o  9342  finsschain  9369  wemaplem3  9560  oemapvali  9696  iunfictbso  10126  enfin2i  10333  fin1a2s  10426  distrlem4pr  11038  mulcmpblnr  11083  prsrlem1  11084  addsrmo  11085  mulsrmo  11086  divdivdiv  11940  divsubdiv  11955  lediv12a  12133  xralrple  13219  seqcaopr  14055  leexp2r  14190  hashbclem  14468  wrd2ind  14739  cshwidxmod  14819  rtrclreclem4  15078  relexpindlem  15080  rtrclind  15082  rlimresb  15579  summo  15731  fsum2dlem  15784  prodmo  15950  fprod2dlem  15994  bezoutlem3  16558  bezoutlem4  16559  qredeu  16675  coprmproddvdslem  16679  prmdvdsncoprmbd  16744  pcqmul  16871  pcadd  16907  pockthg  16924  ramub1lem2  17045  cshwsdisj  17116  mreexexlem4d  17657  issubc3  17860  cofucl  17899  setcmon  18098  setcepi  18099  drsdirfi  18315  poslubmo  18419  posglbmo  18420  grprida  18651  ghmpreima  19219  gaorber  19289  psgnunilem4  19476  psgneu  19485  odcau  19583  pgpssslw  19593  fislw  19604  lsmsubm  19632  efgsfo  19718  pgpfac1  20061  pgpfaclem2  20063  pgpfaclem3  20064  unitgrp  20341  islmodd  20821  lmodprop2d  20879  lsspropd  20973  lbsextlem4  21120  assapropd  21830  evlslem1  22038  mdetunilem8  22555  mdetmul  22559  ppttop  22943  epttop  22945  restbas  23094  iscnp4  23199  cnpco  23203  nrmsep  23293  regsep2  23312  ordthauslem  23319  1stcfb  23381  2ndcctbss  23391  2ndcdisj  23392  2ndcomap  23394  dis2ndc  23396  1stcelcls  23397  nlly2i  23412  islly2  23420  hausllycmp  23430  lly1stc  23432  comppfsc  23468  1stckgenlem  23489  ptbasin  23513  txcls  23540  ptcnp  23558  txlly  23572  txnlly  23573  txtube  23576  txcmplem1  23577  txcmplem2  23578  xkococnlem  23595  basqtop  23647  regr1lem  23675  kqreglem1  23677  kqreglem2  23678  kqnrmlem1  23679  kqnrmlem2  23680  reghmph  23729  nrmhmph  23730  filuni  23821  rnelfmlem  23888  fmufil  23895  fclscf  23961  fclsfnflim  23963  flimfnfcls  23964  uffclsflim  23967  cnpfcfi  23976  cnpfcf  23977  alexsublem  23980  alexsubALTlem3  23985  tgpconncompeqg  24048  ghmcnp  24051  qustgplem  24057  blssps  24361  blss  24362  blcld  24442  metequiv2  24447  met2ndci  24459  prdsxmslem2  24466  txmetcnp  24484  nlmvscnlem1  24623  xrge0tsms  24772  ipcnlem1  25195  iscmet3  25243  metsscmetcld  25265  minveclem3  25379  pmltpc  25401  ovolscalem2  25465  ovolicc2lem5  25472  ovolicc2  25473  nulmbl2  25487  ioombl1  25513  uniioombllem6  25539  uniioombl  25540  vitalilem3  25561  i1faddlem  25644  mbfmullem  25676  itg2const2  25692  itg2split  25700  lhop2  25970  dvfsumrlim  25988  itgsubst  26006  plydivex  26255  plyexmo  26271  ulmbdd  26357  cxploglim  26938  dchrptlem2  27226  lgsquad2lem2  27346  2sqlem5  27383  dchrvmasumif  27464  rpvmasum2  27473  dchrisum0re  27474  dchrisum0lem3  27480  dchrisum0  27481  dchrmusum  27485  dchrvmasum  27486  pntibndlem3  27553  pntlemp  27571  ostth3  27599  nosupbday  27667  nosupbnd1lem1  27670  nosupbnd2  27678  noinfbday  27682  noinfbnd1lem1  27685  noinfbnd2  27693  conway  27761  madebdaylemlrcut  27854  mulsproplem9  28067  mulsuniflem  28092  uzsind  28308  readdscl  28348  legtrid  28516  hlcgreu  28543  mirreu3  28579  opphllem  28660  oppperpex  28678  lnperpex  28728  trgcopy  28729  iscgra1  28735  cgraswap  28745  cgracom  28747  cgratr  28748  flatcgra  28749  acopyeu  28759  ax5seglem9  28862  ax5seg  28863  axcontlem8  28896  axcontlem12  28900  upgrclwlkcompim  29709  wwlksnextwrd  29825  2pthfrgr  30211  frgrnbnb  30220  ablo4  30477  smcnlem  30624  pjhthmo  31229  1stpreimas  32629  xrge0tsmsd  33002  locfinref  33818  xpinpreima2  33884  qqhval2  33959  dya2iocnrect  34259  orvcgteel  34446  orvclteel  34451  cnpconn  35198  txpconn  35200  connpconn  35203  pconnpi1  35205  iccllysconn  35218  rellysconn  35219  cvmcov2  35243  cvmliftmolem2  35250  cvmliftmo  35252  cvmliftlem15  35266  cvmliftpht  35286  cvmlift3lem2  35288  cgrextend  35972  btwnouttr2  35986  btwnexch2  35987  cgrxfr  36019  lineext  36040  btwnconn1lem5  36055  btwnconn1lem13  36063  btwnconn3  36067  segletr  36078  segleantisym  36079  outsideofeq  36094  outsidele  36096  lineunray  36111  refssfne  36322  neibastop2lem  36324  neibastop2  36325  weiunpo  36429  unblimceq0lem  36470  knoppndvlem22  36497  mblfinlem3  37629  mblfinlem4  37630  cnambfre  37638  itg2addnclem  37641  areacirclem5  37682  istotbnd3  37741  crngm4  37973  cvlcvr1  39303  4atlem12  39577  cdlemb  39759  paddasslem10  39794  paddasslem12  39796  paddasslem13  39797  lhpexle3lem  39976  cdlemd4  40166  cdlemefs32sn1aw  40379  cdleme43fsv1snlem  40385  cdleme32d  40409  cdleme32f  40411  cdleme40m  40432  cdleme40n  40433  cdleme50trn2  40516  cdlemftr3  40530  cdlemm10N  41083  dihvalcqpre  41200  dihopelvalcpre  41213  dihmeetlem1N  41255  dihglblem5apreN  41256  dihmeetlem4preN  41271  dihjat1lem  41393  mapd0  41630  mapdh9a  41754  nna4b4nsq  42630  mzpmfp  42717  mzpcompact2lem  42721  diophin  42742  pellexlem3  42801  pellex  42805  pell14qrmulcl  42833  jm2.19lem3  42962  jm2.25  42970  jm2.27b  42977  fnwe2lem2  43022  hbtlem2  43095  hbtlem5  43099  gsumws3  44167  gsumws4  44168  mnuprdlem1  44244  mnuprdlem2  44245  mnuprdlem4  44247  fnchoice  45001  stoweidlem53  46030  stoweidlem61  46038  qndenserrnbllem  46271  bgoldbtbnd  47771  cycldlenngric  47889  grtrimap  47908  isubgr3stgrlem6  47931  prsthinc  49298