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 486	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜃)
2	1	ad2antll 728	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 206  df-an 398

This theorem is referenced by:  prproe  4907  f1prex  7282  fliftfun  7309  fprresex  8295  wfrlem17OLD  8325  naddssim  8684  mapdom2  9148  domunfican  9320  fofinf1o  9327  finsschain  9359  wemaplem3  9543  oemapvali  9679  iunfictbso  10109  enfin2i  10316  fin1a2s  10409  distrlem4pr  11021  mulcmpblnr  11066  prsrlem1  11067  addsrmo  11068  mulsrmo  11069  divdivdiv  11915  divsubdiv  11930  lediv12a  12107  xralrple  13184  seqcaopr  14005  leexp2r  14139  hashbclem  14411  wrd2ind  14673  cshwidxmod  14753  rtrclreclem4  15008  relexpindlem  15010  rtrclind  15012  rlimresb  15509  summo  15663  fsum2dlem  15716  prodmo  15880  fprod2dlem  15924  bezoutlem3  16483  bezoutlem4  16484  qredeu  16595  coprmproddvdslem  16599  prmdvdsncoprmbd  16663  pcqmul  16786  pcadd  16822  pockthg  16839  ramub1lem2  16960  cshwsdisj  17032  mreexexlem4d  17591  issubc3  17799  cofucl  17838  setcmon  18037  setcepi  18038  drsdirfi  18258  poslubmo  18364  posglbmo  18365  grprida  18594  ghmpreima  19114  gaorber  19172  psgnunilem4  19365  psgneu  19374  odcau  19472  pgpssslw  19482  fislw  19493  lsmsubm  19521  efgsfo  19607  pgpfac1  19950  pgpfaclem2  19952  pgpfaclem3  19953  unitgrp  20197  islmodd  20477  lmodprop2d  20534  lsspropd  20628  lbsextlem4  20774  assapropd  21426  evlslem1  21645  mdetunilem8  22121  mdetmul  22125  ppttop  22510  epttop  22512  restbas  22662  iscnp4  22767  cnpco  22771  nrmsep  22861  regsep2  22880  ordthauslem  22887  1stcfb  22949  2ndcctbss  22959  2ndcdisj  22960  2ndcomap  22962  dis2ndc  22964  1stcelcls  22965  nlly2i  22980  islly2  22988  hausllycmp  22998  lly1stc  23000  comppfsc  23036  1stckgenlem  23057  ptbasin  23081  txcls  23108  ptcnp  23126  txlly  23140  txnlly  23141  txtube  23144  txcmplem1  23145  txcmplem2  23146  xkococnlem  23163  basqtop  23215  regr1lem  23243  kqreglem1  23245  kqreglem2  23246  kqnrmlem1  23247  kqnrmlem2  23248  reghmph  23297  nrmhmph  23298  filuni  23389  rnelfmlem  23456  fmufil  23463  fclscf  23529  fclsfnflim  23531  flimfnfcls  23532  uffclsflim  23535  cnpfcfi  23544  cnpfcf  23545  alexsublem  23548  alexsubALTlem3  23553  tgpconncompeqg  23616  ghmcnp  23619  qustgplem  23625  blssps  23930  blss  23931  blcld  24014  metequiv2  24019  met2ndci  24031  prdsxmslem2  24038  txmetcnp  24056  nlmvscnlem1  24203  xrge0tsms  24350  ipcnlem1  24762  iscmet3  24810  metsscmetcld  24832  minveclem3  24946  pmltpc  24967  ovolscalem2  25031  ovolicc2lem5  25038  ovolicc2  25039  nulmbl2  25053  ioombl1  25079  uniioombllem6  25105  uniioombl  25106  vitalilem3  25127  i1faddlem  25210  mbfmullem  25243  itg2const2  25259  itg2split  25267  lhop2  25532  dvfsumrlim  25548  itgsubst  25566  plydivex  25810  plyexmo  25826  ulmbdd  25910  cxploglim  26482  dchrptlem2  26768  lgsquad2lem2  26888  2sqlem5  26925  dchrvmasumif  27006  rpvmasum2  27015  dchrisum0re  27016  dchrisum0lem3  27022  dchrisum0  27023  dchrmusum  27027  dchrvmasum  27028  pntibndlem3  27095  pntlemp  27113  ostth3  27141  nosupbday  27208  nosupbnd1lem1  27211  nosupbnd2  27219  noinfbday  27223  noinfbnd1lem1  27226  noinfbnd2  27234  conway  27300  madebdaylemlrcut  27393  mulsproplem9  27580  mulsuniflem  27604  legtrid  27842  hlcgreu  27869  mirreu3  27905  opphllem  27986  oppperpex  28004  lnperpex  28054  trgcopy  28055  iscgra1  28061  cgraswap  28071  cgracom  28073  cgratr  28074  flatcgra  28075  acopyeu  28085  ax5seglem9  28195  ax5seg  28196  axcontlem8  28229  axcontlem12  28233  upgrclwlkcompim  29038  wwlksnextwrd  29151  2pthfrgr  29537  frgrnbnb  29546  ablo4  29803  smcnlem  29950  pjhthmo  30555  1stpreimas  31927  xrge0tsmsd  32209  locfinref  32821  xpinpreima2  32887  qqhval2  32962  dya2iocnrect  33280  orvcgteel  33466  orvclteel  33471  cnpconn  34221  txpconn  34223  connpconn  34226  pconnpi1  34228  iccllysconn  34241  rellysconn  34242  cvmcov2  34266  cvmliftmolem2  34273  cvmliftmo  34275  cvmliftlem15  34289  cvmliftpht  34309  cvmlift3lem2  34311  cgrextend  34980  btwnouttr2  34994  btwnexch2  34995  cgrxfr  35027  lineext  35048  btwnconn1lem5  35063  btwnconn1lem13  35071  btwnconn3  35075  segletr  35086  segleantisym  35087  outsideofeq  35102  outsidele  35104  lineunray  35119  refssfne  35243  neibastop2lem  35245  neibastop2  35246  unblimceq0lem  35382  knoppndvlem22  35409  mblfinlem3  36527  mblfinlem4  36528  cnambfre  36536  itg2addnclem  36539  areacirclem5  36580  istotbnd3  36639  crngm4  36871  cvlcvr1  38209  4atlem12  38483  cdlemb  38665  paddasslem10  38700  paddasslem12  38702  paddasslem13  38703  lhpexle3lem  38882  cdlemd4  39072  cdlemefs32sn1aw  39285  cdleme43fsv1snlem  39291  cdleme32d  39315  cdleme32f  39317  cdleme40m  39338  cdleme40n  39339  cdleme50trn2  39422  cdlemftr3  39436  cdlemm10N  39989  dihvalcqpre  40106  dihopelvalcpre  40119  dihmeetlem1N  40161  dihglblem5apreN  40162  dihmeetlem4preN  40177  dihjat1lem  40299  mapd0  40536  mapdh9a  40660  nna4b4nsq  41402  mzpmfp  41485  mzpcompact2lem  41489  diophin  41510  pellexlem3  41569  pellex  41573  pell14qrmulcl  41601  jm2.19lem3  41730  jm2.25  41738  jm2.27b  41745  fnwe2lem2  41793  hbtlem2  41866  hbtlem5  41870  gsumws3  42948  gsumws4  42949  mnuprdlem1  43031  mnuprdlem2  43032  mnuprdlem4  43034  fnchoice  43713  stoweidlem53  44769  stoweidlem61  44777  qndenserrnbllem  45010  bgoldbtbnd  46477  prsthinc  47674