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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  prproe  4798  f1prex  7018  fliftfun  7044  wfrlem17  7954  mapdom2  8672  domunfican  8775  fofinf1o  8783  finsschain  8815  wemaplem3  8996  oemapvali  9131  iunfictbso  9525  enfin2i  9732  fin1a2s  9825  distrlem4pr  10437  mulcmpblnr  10482  prsrlem1  10483  addsrmo  10484  mulsrmo  10485  divdivdiv  11330  divsubdiv  11345  lediv12a  11522  xralrple  12586  seqcaopr  13403  leexp2r  13534  hashbclem  13806  wrd2ind  14076  cshwidxmod  14156  rtrclreclem4  14412  relexpindlem  14414  rtrclind  14416  rlimresb  14914  summo  15066  fsum2dlem  15117  prodmo  15282  fprod2dlem  15326  bezoutlem3  15879  bezoutlem4  15880  qredeu  15992  coprmproddvdslem  15996  pcqmul  16180  pcadd  16215  pockthg  16232  ramub1lem2  16353  cshwsdisj  16424  mreexexlem4d  16910  issubc3  17111  cofucl  17150  setcmon  17339  setcepi  17340  drsdirfi  17540  poslubmo  17748  posglbmo  17749  grpridd  17877  ghmpreima  18372  gaorber  18430  psgnunilem4  18617  psgneu  18626  odcau  18721  pgpssslw  18731  fislw  18742  lsmsubm  18770  efgsfo  18857  pgpfac1  19195  pgpfaclem2  19197  pgpfaclem3  19198  unitgrp  19413  islmodd  19633  lmodprop2d  19689  lsspropd  19782  lbsextlem4  19926  assapropd  20558  evlslem1  20754  mdetunilem8  21224  mdetmul  21228  ppttop  21612  epttop  21614  restbas  21763  iscnp4  21868  cnpco  21872  nrmsep  21962  regsep2  21981  ordthauslem  21988  1stcfb  22050  2ndcctbss  22060  2ndcdisj  22061  2ndcomap  22063  dis2ndc  22065  1stcelcls  22066  nlly2i  22081  islly2  22089  hausllycmp  22099  lly1stc  22101  comppfsc  22137  1stckgenlem  22158  ptbasin  22182  txcls  22209  ptcnp  22227  txlly  22241  txnlly  22242  txtube  22245  txcmplem1  22246  txcmplem2  22247  xkococnlem  22264  basqtop  22316  regr1lem  22344  kqreglem1  22346  kqreglem2  22347  kqnrmlem1  22348  kqnrmlem2  22349  reghmph  22398  nrmhmph  22399  filuni  22490  rnelfmlem  22557  fmufil  22564  fclscf  22630  fclsfnflim  22632  flimfnfcls  22633  uffclsflim  22636  cnpfcfi  22645  cnpfcf  22646  alexsublem  22649  alexsubALTlem3  22654  tgpconncompeqg  22717  ghmcnp  22720  qustgplem  22726  blssps  23031  blss  23032  blcld  23112  metequiv2  23117  met2ndci  23129  prdsxmslem2  23136  txmetcnp  23154  nlmvscnlem1  23292  xrge0tsms  23439  ipcnlem1  23849  iscmet3  23897  metsscmetcld  23919  minveclem3  24033  pmltpc  24054  ovolscalem2  24118  ovolicc2lem5  24125  ovolicc2  24126  nulmbl2  24140  ioombl1  24166  uniioombllem6  24192  uniioombl  24193  vitalilem3  24214  i1faddlem  24297  mbfmullem  24329  itg2const2  24345  itg2split  24353  lhop2  24618  dvfsumrlim  24634  itgsubst  24652  plydivex  24893  plyexmo  24909  ulmbdd  24993  cxploglim  25563  dchrptlem2  25849  lgsquad2lem2  25969  2sqlem5  26006  dchrvmasumif  26087  rpvmasum2  26096  dchrisum0re  26097  dchrisum0lem3  26103  dchrisum0  26104  dchrmusum  26108  dchrvmasum  26109  pntibndlem3  26176  pntlemp  26194  ostth3  26222  legtrid  26385  hlcgreu  26412  mirreu3  26448  opphllem  26529  oppperpex  26547  lnperpex  26597  trgcopy  26598  iscgra1  26604  cgraswap  26614  cgracom  26616  cgratr  26617  flatcgra  26618  acopyeu  26628  ax5seglem9  26731  ax5seg  26732  axcontlem8  26765  axcontlem12  26769  upgrclwlkcompim  27570  wwlksnextwrd  27683  2pthfrgr  28069  frgrnbnb  28078  ablo4  28333  smcnlem  28480  pjhthmo  29085  1stpreimas  30465  xrge0tsmsd  30742  locfinref  31194  xpinpreima2  31260  qqhval2  31333  dya2iocnrect  31649  orvcgteel  31835  orvclteel  31840  cnpconn  32590  txpconn  32592  connpconn  32595  pconnpi1  32597  iccllysconn  32610  rellysconn  32611  cvmcov2  32635  cvmliftmolem2  32642  cvmliftmo  32644  cvmliftlem15  32658  cvmliftpht  32678  cvmlift3lem2  32680  nosupbnd1lem1  33321  nosupbnd2  33329  conway  33377  cgrextend  33582  btwnouttr2  33596  btwnexch2  33597  cgrxfr  33629  lineext  33650  btwnconn1lem5  33665  btwnconn1lem13  33673  btwnconn3  33677  segletr  33688  segleantisym  33689  outsideofeq  33704  outsidele  33706  lineunray  33721  refssfne  33819  neibastop2lem  33821  neibastop2  33822  unblimceq0lem  33958  knoppndvlem22  33985  mblfinlem3  35096  mblfinlem4  35097  cnambfre  35105  itg2addnclem  35108  areacirclem5  35149  istotbnd3  35209  crngm4  35441  cvlcvr1  36635  4atlem12  36908  cdlemb  37090  paddasslem10  37125  paddasslem12  37127  paddasslem13  37128  lhpexle3lem  37307  cdlemd4  37497  cdlemefs32sn1aw  37710  cdleme43fsv1snlem  37716  cdleme32d  37740  cdleme32f  37742  cdleme40m  37763  cdleme40n  37764  cdleme50trn2  37847  cdlemftr3  37861  cdlemm10N  38414  dihvalcqpre  38531  dihopelvalcpre  38544  dihmeetlem1N  38586  dihglblem5apreN  38587  dihmeetlem4preN  38602  dihjat1lem  38724  mapd0  38961  mapdh9a  39085  mzpmfp  39688  mzpcompact2lem  39692  diophin  39713  pellexlem3  39772  pellex  39776  pell14qrmulcl  39804  jm2.19lem3  39932  jm2.25  39940  jm2.27b  39947  fnwe2lem2  39995  hbtlem2  40068  hbtlem5  40072  gsumws3  40902  gsumws4  40903  mnuprdlem1  40980  mnuprdlem2  40981  mnuprdlem4  40983  fnchoice  41658  stoweidlem53  42695  stoweidlem61  42703  qndenserrnbllem  42936  bgoldbtbnd  44327