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  4854  f1prex  7212  fliftfun  7240  fprresex  8234  nnaordex2  8548  naddssim  8594  mapdom2  9055  domunfican  9200  fofinf1o  9210  finsschain  9237  wemaplem3  9428  oemapvali  9568  iunfictbso  9996  enfin2i  10203  fin1a2s  10296  distrlem4pr  10908  mulcmpblnr  10953  prsrlem1  10954  addsrmo  10955  mulsrmo  10956  divdivdiv  11813  divsubdiv  11828  lediv12a  12006  xralrple  13095  seqcaopr  13934  leexp2r  14069  hashbclem  14347  wrd2ind  14617  cshwidxmod  14697  rtrclreclem4  14955  relexpindlem  14957  rtrclind  14959  rlimresb  15459  summo  15611  fsum2dlem  15664  prodmo  15830  fprod2dlem  15874  bezoutlem3  16439  bezoutlem4  16440  qredeu  16556  coprmproddvdslem  16560  prmdvdsncoprmbd  16625  pcqmul  16752  pcadd  16788  pockthg  16805  ramub1lem2  16926  cshwsdisj  16997  mreexexlem4d  17540  issubc3  17743  cofucl  17782  setcmon  17981  setcepi  17982  drsdirfi  18198  poslubmo  18302  posglbmo  18303  grprida  18536  ghmpreima  19104  gaorber  19174  psgnunilem4  19363  psgneu  19372  odcau  19470  pgpssslw  19480  fislw  19491  lsmsubm  19519  efgsfo  19605  pgpfac1  19948  pgpfaclem2  19950  pgpfaclem3  19951  unitgrp  20255  islmodd  20753  lmodprop2d  20811  lsspropd  20905  lbsextlem4  21052  assapropd  21763  evlslem1  21971  mdetunilem8  22488  mdetmul  22492  ppttop  22876  epttop  22878  restbas  23027  iscnp4  23132  cnpco  23136  nrmsep  23226  regsep2  23245  ordthauslem  23252  1stcfb  23314  2ndcctbss  23324  2ndcdisj  23325  2ndcomap  23327  dis2ndc  23329  1stcelcls  23330  nlly2i  23345  islly2  23353  hausllycmp  23363  lly1stc  23365  comppfsc  23401  1stckgenlem  23422  ptbasin  23446  txcls  23473  ptcnp  23491  txlly  23505  txnlly  23506  txtube  23509  txcmplem1  23510  txcmplem2  23511  xkococnlem  23528  basqtop  23580  regr1lem  23608  kqreglem1  23610  kqreglem2  23611  kqnrmlem1  23612  kqnrmlem2  23613  reghmph  23662  nrmhmph  23663  filuni  23754  rnelfmlem  23821  fmufil  23828  fclscf  23894  fclsfnflim  23896  flimfnfcls  23897  uffclsflim  23900  cnpfcfi  23909  cnpfcf  23910  alexsublem  23913  alexsubALTlem3  23918  tgpconncompeqg  23981  ghmcnp  23984  qustgplem  23990  blssps  24293  blss  24294  blcld  24374  metequiv2  24379  met2ndci  24391  prdsxmslem2  24398  txmetcnp  24416  nlmvscnlem1  24555  xrge0tsms  24704  ipcnlem1  25126  iscmet3  25174  metsscmetcld  25196  minveclem3  25310  pmltpc  25332  ovolscalem2  25396  ovolicc2lem5  25403  ovolicc2  25404  nulmbl2  25418  ioombl1  25444  uniioombllem6  25470  uniioombl  25471  vitalilem3  25492  i1faddlem  25575  mbfmullem  25607  itg2const2  25623  itg2split  25631  lhop2  25901  dvfsumrlim  25919  itgsubst  25937  plydivex  26186  plyexmo  26202  ulmbdd  26288  cxploglim  26869  dchrptlem2  27157  lgsquad2lem2  27277  2sqlem5  27314  dchrvmasumif  27395  rpvmasum2  27404  dchrisum0re  27405  dchrisum0lem3  27411  dchrisum0  27412  dchrmusum  27416  dchrvmasum  27417  pntibndlem3  27484  pntlemp  27502  ostth3  27530  nosupbday  27598  nosupbnd1lem1  27601  nosupbnd2  27609  noinfbday  27613  noinfbnd1lem1  27616  noinfbnd2  27624  conway  27694  madebdaylemlrcut  27798  mulsproplem9  28017  mulsuniflem  28042  uzsind  28283  readdscl  28355  legtrid  28523  hlcgreu  28550  mirreu3  28586  opphllem  28667  oppperpex  28685  lnperpex  28735  trgcopy  28736  iscgra1  28742  cgraswap  28752  cgracom  28754  cgratr  28755  flatcgra  28756  acopyeu  28766  ax5seglem9  28869  ax5seg  28870  axcontlem8  28903  axcontlem12  28907  upgrclwlkcompim  29713  wwlksnextwrd  29829  2pthfrgr  30215  frgrnbnb  30224  ablo4  30481  smcnlem  30628  pjhthmo  31233  1stpreimas  32639  xrge0tsmsd  33010  locfinref  33822  xpinpreima2  33888  qqhval2  33963  dya2iocnrect  34262  orvcgteel  34449  orvclteel  34454  cnpconn  35220  txpconn  35222  connpconn  35225  pconnpi1  35227  iccllysconn  35240  rellysconn  35241  cvmcov2  35265  cvmliftmolem2  35272  cvmliftmo  35274  cvmliftlem15  35288  cvmliftpht  35308  cvmlift3lem2  35310  cgrextend  35999  btwnouttr2  36013  btwnexch2  36014  cgrxfr  36046  lineext  36067  btwnconn1lem5  36082  btwnconn1lem13  36090  btwnconn3  36094  segletr  36105  segleantisym  36106  outsideofeq  36121  outsidele  36123  lineunray  36138  refssfne  36349  neibastop2lem  36351  neibastop2  36352  weiunpo  36456  unblimceq0lem  36497  knoppndvlem22  36524  mblfinlem3  37656  mblfinlem4  37657  cnambfre  37665  itg2addnclem  37668  areacirclem5  37709  istotbnd3  37768  crngm4  38000  cvlcvr1  39335  4atlem12  39608  cdlemb  39790  paddasslem10  39825  paddasslem12  39827  paddasslem13  39828  lhpexle3lem  40007  cdlemd4  40197  cdlemefs32sn1aw  40410  cdleme43fsv1snlem  40416  cdleme32d  40440  cdleme32f  40442  cdleme40m  40463  cdleme40n  40464  cdleme50trn2  40547  cdlemftr3  40561  cdlemm10N  41114  dihvalcqpre  41231  dihopelvalcpre  41244  dihmeetlem1N  41286  dihglblem5apreN  41287  dihmeetlem4preN  41302  dihjat1lem  41424  mapd0  41661  mapdh9a  41785  nna4b4nsq  42650  mzpmfp  42737  mzpcompact2lem  42741  diophin  42762  pellexlem3  42821  pellex  42825  pell14qrmulcl  42853  jm2.19lem3  42981  jm2.25  42989  jm2.27b  42996  fnwe2lem2  43041  hbtlem2  43114  hbtlem5  43118  gsumws3  44186  gsumws4  44187  mnuprdlem1  44262  mnuprdlem2  44263  mnuprdlem4  44265  fnchoice  45023  stoweidlem53  46048  stoweidlem61  46056  qndenserrnbllem  46289  bgoldbtbnd  47807  cycldlenngric  47926  grtrimap  47946  isubgr3stgrlem6  47969  prsthinc  49463