Theorem simprrr 793

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

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  prproe  4869  f1prex  7282  fliftfun  7310  fprresex  8306  nnaordex2  8624  naddssim  8671  mapdom2  9135  domunfican  9280  fofinf1o  9288  finsschain  9315  wemaplem3  9509  oemapvali  9652  iunfictbso  10097  enfin2i  10304  fin1a2s  10397  distrlem4pr  11010  mulcmpblnr  11055  prsrlem1  11056  addsrmo  11057  mulsrmo  11058  divdivdiv  11915  divsubdiv  11930  lediv12a  12107  xralrple  13230  seqcaopr  14074  leexp2r  14209  hashbclem  14488  wrd2ind  14759  cshwidxmod  14839  rtrclreclem4  15097  relexpindlem  15099  rtrclind  15101  rlimresb  15615  summo  15767  fsum2dlem  15820  prodmo  15989  fprod2dlem  16033  bezoutlem3  16598  bezoutlem4  16599  qredeu  16715  coprmproddvdslem  16719  prmdvdsncoprmbd  16785  pcqmul  16912  pcadd  16948  pockthg  16965  ramub1lem2  17086  cshwsdisj  17157  mreexexlem4d  17702  issubc3  17905  cofucl  17944  setcmon  18143  setcepi  18144  drsdirfi  18360  poslubmo  18464  posglbmo  18465  grprida  18732  ghmpreima  19307  gaorber  19377  psgnunilem4  19566  psgneu  19575  odcau  19673  pgpssslw  19683  fislw  19694  lsmsubm  19722  efgsfo  19808  pgpfac1  20151  pgpfaclem2  20153  pgpfaclem3  20154  unitgrp  20464  islmodd  20966  lmodprop2d  21024  lsspropd  21117  lbsextlem4  21264  assapropd  22000  evlslem1  22212  mdetunilem8  22755  mdetmul  22759  ppttop  23143  epttop  23145  restbas  23294  iscnp4  23399  cnpco  23403  nrmsep  23493  regsep2  23512  ordthauslem  23519  1stcfb  23581  2ndcctbss  23591  2ndcdisj  23592  2ndcomap  23594  dis2ndc  23596  1stcelcls  23597  nlly2i  23612  islly2  23620  hausllycmp  23630  lly1stc  23632  comppfsc  23668  1stckgenlem  23689  ptbasin  23713  txcls  23740  ptcnp  23758  txlly  23772  txnlly  23773  txtube  23776  txcmplem1  23777  txcmplem2  23778  xkococnlem  23795  basqtop  23847  regr1lem  23875  kqreglem1  23877  kqreglem2  23878  kqnrmlem1  23879  kqnrmlem2  23880  reghmph  23929  nrmhmph  23930  filuni  24021  rnelfmlem  24088  fmufil  24095  fclscf  24161  fclsfnflim  24163  flimfnfcls  24164  uffclsflim  24167  cnpfcfi  24176  cnpfcf  24177  alexsublem  24180  alexsubALTlem3  24185  tgpconncompeqg  24248  ghmcnp  24251  qustgplem  24257  blssps  24560  blss  24561  blcld  24641  metequiv2  24646  met2ndci  24658  prdsxmslem2  24665  txmetcnp  24683  nlmvscnlem1  24822  xrge0tsms  24971  ipcnlem1  25383  iscmet3  25431  metsscmetcld  25453  minveclem3  25567  pmltpc  25588  ovolscalem2  25652  ovolicc2lem5  25659  ovolicc2  25660  nulmbl2  25674  ioombl1  25700  uniioombllem6  25726  uniioombl  25727  vitalilem3  25748  i1faddlem  25831  mbfmullem  25863  itg2const2  25879  itg2split  25887  lhop2  26153  dvfsumrlim  26169  itgsubst  26187  plydivex  26437  plyexmo  26453  ulmbdd  26537  cxploglim  27118  dchrptlem2  27405  lgsquad2lem2  27525  2sqlem5  27562  dchrvmasumif  27643  rpvmasum2  27652  dchrisum0re  27653  dchrisum0lem3  27659  dchrisum0  27660  dchrmusum  27664  dchrvmasum  27665  pntibndlem3  27732  pntlemp  27750  ostth3  27778  nosupbday  27845  nosupbnd1lem1  27848  nosupbnd2  27856  noinfbday  27860  noinfbnd1lem1  27863  noinfbnd2  27871  conway  27948  madebdaylemlrcut  28068  mulsproplem9  28293  mulsuniflem  28318  uzsind  28574  bdayfinbndlem1  28636  readdscl  28668  legtrid  28836  hlcgreu  28866  mirreu3  28907  opphllem  28991  oppperpex  29009  lnperpex  29086  trgcopy  29088  iscgra1  29094  cgraswap  29104  cgracom  29106  cgratr  29107  flatcgra  29108  acopyeu  29118  ax5seglem9  29253  ax5seg  29254  axcontlem8  29287  axcontlem12  29291  upgrclwlkcompim  30096  wwlksnextwrd  30212  2pthfrgr  30601  frgrnbnb  30610  ablo4  30868  smcnlem  31015  pjhthmo  31620  1stpreimas  33017  xrge0tsmsd  33359  locfinref  34197  xpinpreima2  34263  qqhval2  34338  dya2iocnrect  34637  orvcgteel  34824  orvclteel  34829  cnpconn  35688  txpconn  35690  connpconn  35693  pconnpi1  35695  iccllysconn  35708  rellysconn  35709  cvmcov2  35733  cvmliftmolem2  35740  cvmliftmo  35742  cvmliftlem15  35756  cvmliftpht  35776  cvmlift3lem2  35778  cgrextend  36466  btwnouttr2  36480  btwnexch2  36481  cgrxfr  36513  lineext  36534  btwnconn1lem5  36549  btwnconn1lem13  36557  btwnconn3  36561  segletr  36572  segleantisym  36573  outsideofeq  36588  outsidele  36590  lineunray  36605  refssfne  36835  neibastop2lem  36837  neibastop2  36838  weiunpo  36942  unblimceq0lem  37061  knoppndvlem22  37088  mblfinlem3  38276  mblfinlem4  38277  cnambfre  38285  itg2addnclem  38288  areacirclem5  38329  istotbnd3  38388  crngm4  38620  cvlcvr1  40081  4atlem12  40354  cdlemb  40536  paddasslem10  40571  paddasslem12  40573  paddasslem13  40574  lhpexle3lem  40753  cdlemd4  40943  cdlemefs32sn1aw  41156  cdleme43fsv1snlem  41162  cdleme32d  41186  cdleme32f  41188  cdleme40m  41209  cdleme40n  41210  cdleme50trn2  41293  cdlemftr3  41307  cdlemm10N  41860  dihvalcqpre  41977  dihopelvalcpre  41990  dihmeetlem1N  42032  dihglblem5apreN  42033  dihmeetlem4preN  42048  dihjat1lem  42170  mapd0  42407  mapdh9a  42531  nna4b4nsq  43362  mzpmfp  43448  mzpcompact2lem  43452  diophin  43473  pellexlem3  43528  pellex  43532  pell14qrmulcl  43560  jm2.19lem3  43688  jm2.25  43696  jm2.27b  43703  fnwe2lem2  43748  hbtlem2  43821  hbtlem5  43825  gsumws3  44892  gsumws4  44893  mnuprdlem1  44952  mnuprdlem2  44953  mnuprdlem4  44955  fnchoice  45719  stoweidlem53  46737  stoweidlem61  46745  qndenserrnbllem  46978  bgoldbtbnd  48541  cycldlenngric  48660  grtrimap  48680  isubgr3stgrlem6  48703  prsthinc  50209