Theorem simprrr 782

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  4905  f1prex  7304  fliftfun  7332  fprresex  8335  wfrlem17OLD  8365  nnaordex2  8677  naddssim  8723  mapdom2  9188  domunfican  9361  fofinf1o  9372  finsschain  9399  wemaplem3  9588  oemapvali  9724  iunfictbso  10154  enfin2i  10361  fin1a2s  10454  distrlem4pr  11066  mulcmpblnr  11111  prsrlem1  11112  addsrmo  11113  mulsrmo  11114  divdivdiv  11968  divsubdiv  11983  lediv12a  12161  xralrple  13247  seqcaopr  14080  leexp2r  14214  hashbclem  14491  wrd2ind  14761  cshwidxmod  14841  rtrclreclem4  15100  relexpindlem  15102  rtrclind  15104  rlimresb  15601  summo  15753  fsum2dlem  15806  prodmo  15972  fprod2dlem  16016  bezoutlem3  16578  bezoutlem4  16579  qredeu  16695  coprmproddvdslem  16699  prmdvdsncoprmbd  16764  pcqmul  16891  pcadd  16927  pockthg  16944  ramub1lem2  17065  cshwsdisj  17136  mreexexlem4d  17690  issubc3  17894  cofucl  17933  setcmon  18132  setcepi  18133  drsdirfi  18351  poslubmo  18456  posglbmo  18457  grprida  18688  ghmpreima  19256  gaorber  19326  psgnunilem4  19515  psgneu  19524  odcau  19622  pgpssslw  19632  fislw  19643  lsmsubm  19671  efgsfo  19757  pgpfac1  20100  pgpfaclem2  20102  pgpfaclem3  20103  unitgrp  20383  islmodd  20864  lmodprop2d  20922  lsspropd  21016  lbsextlem4  21163  assapropd  21892  evlslem1  22106  mdetunilem8  22625  mdetmul  22629  ppttop  23014  epttop  23016  restbas  23166  iscnp4  23271  cnpco  23275  nrmsep  23365  regsep2  23384  ordthauslem  23391  1stcfb  23453  2ndcctbss  23463  2ndcdisj  23464  2ndcomap  23466  dis2ndc  23468  1stcelcls  23469  nlly2i  23484  islly2  23492  hausllycmp  23502  lly1stc  23504  comppfsc  23540  1stckgenlem  23561  ptbasin  23585  txcls  23612  ptcnp  23630  txlly  23644  txnlly  23645  txtube  23648  txcmplem1  23649  txcmplem2  23650  xkococnlem  23667  basqtop  23719  regr1lem  23747  kqreglem1  23749  kqreglem2  23750  kqnrmlem1  23751  kqnrmlem2  23752  reghmph  23801  nrmhmph  23802  filuni  23893  rnelfmlem  23960  fmufil  23967  fclscf  24033  fclsfnflim  24035  flimfnfcls  24036  uffclsflim  24039  cnpfcfi  24048  cnpfcf  24049  alexsublem  24052  alexsubALTlem3  24057  tgpconncompeqg  24120  ghmcnp  24123  qustgplem  24129  blssps  24434  blss  24435  blcld  24518  metequiv2  24523  met2ndci  24535  prdsxmslem2  24542  txmetcnp  24560  nlmvscnlem1  24707  xrge0tsms  24856  ipcnlem1  25279  iscmet3  25327  metsscmetcld  25349  minveclem3  25463  pmltpc  25485  ovolscalem2  25549  ovolicc2lem5  25556  ovolicc2  25557  nulmbl2  25571  ioombl1  25597  uniioombllem6  25623  uniioombl  25624  vitalilem3  25645  i1faddlem  25728  mbfmullem  25760  itg2const2  25776  itg2split  25784  lhop2  26054  dvfsumrlim  26072  itgsubst  26090  plydivex  26339  plyexmo  26355  ulmbdd  26441  cxploglim  27021  dchrptlem2  27309  lgsquad2lem2  27429  2sqlem5  27466  dchrvmasumif  27547  rpvmasum2  27556  dchrisum0re  27557  dchrisum0lem3  27563  dchrisum0  27564  dchrmusum  27568  dchrvmasum  27569  pntibndlem3  27636  pntlemp  27654  ostth3  27682  nosupbday  27750  nosupbnd1lem1  27753  nosupbnd2  27761  noinfbday  27765  noinfbnd1lem1  27768  noinfbnd2  27776  conway  27844  madebdaylemlrcut  27937  mulsproplem9  28150  mulsuniflem  28175  uzsind  28391  readdscl  28431  legtrid  28599  hlcgreu  28626  mirreu3  28662  opphllem  28743  oppperpex  28761  lnperpex  28811  trgcopy  28812  iscgra1  28818  cgraswap  28828  cgracom  28830  cgratr  28831  flatcgra  28832  acopyeu  28842  ax5seglem9  28952  ax5seg  28953  axcontlem8  28986  axcontlem12  28990  upgrclwlkcompim  29801  wwlksnextwrd  29917  2pthfrgr  30303  frgrnbnb  30312  ablo4  30569  smcnlem  30716  pjhthmo  31321  1stpreimas  32715  xrge0tsmsd  33065  locfinref  33840  xpinpreima2  33906  qqhval2  33983  dya2iocnrect  34283  orvcgteel  34470  orvclteel  34475  cnpconn  35235  txpconn  35237  connpconn  35240  pconnpi1  35242  iccllysconn  35255  rellysconn  35256  cvmcov2  35280  cvmliftmolem2  35287  cvmliftmo  35289  cvmliftlem15  35303  cvmliftpht  35323  cvmlift3lem2  35325  cgrextend  36009  btwnouttr2  36023  btwnexch2  36024  cgrxfr  36056  lineext  36077  btwnconn1lem5  36092  btwnconn1lem13  36100  btwnconn3  36104  segletr  36115  segleantisym  36116  outsideofeq  36131  outsidele  36133  lineunray  36148  refssfne  36359  neibastop2lem  36361  neibastop2  36362  weiunpo  36466  unblimceq0lem  36507  knoppndvlem22  36534  mblfinlem3  37666  mblfinlem4  37667  cnambfre  37675  itg2addnclem  37678  areacirclem5  37719  istotbnd3  37778  crngm4  38010  cvlcvr1  39340  4atlem12  39614  cdlemb  39796  paddasslem10  39831  paddasslem12  39833  paddasslem13  39834  lhpexle3lem  40013  cdlemd4  40203  cdlemefs32sn1aw  40416  cdleme43fsv1snlem  40422  cdleme32d  40446  cdleme32f  40448  cdleme40m  40469  cdleme40n  40470  cdleme50trn2  40553  cdlemftr3  40567  cdlemm10N  41120  dihvalcqpre  41237  dihopelvalcpre  41250  dihmeetlem1N  41292  dihglblem5apreN  41293  dihmeetlem4preN  41308  dihjat1lem  41430  mapd0  41667  mapdh9a  41791  nna4b4nsq  42670  mzpmfp  42758  mzpcompact2lem  42762  diophin  42783  pellexlem3  42842  pellex  42846  pell14qrmulcl  42874  jm2.19lem3  43003  jm2.25  43011  jm2.27b  43018  fnwe2lem2  43063  hbtlem2  43136  hbtlem5  43140  gsumws3  44209  gsumws4  44210  mnuprdlem1  44291  mnuprdlem2  44292  mnuprdlem4  44294  fnchoice  45034  stoweidlem53  46068  stoweidlem61  46076  qndenserrnbllem  46309  bgoldbtbnd  47796  grtrimap  47915  isubgr3stgrlem6  47938  prsthinc  49111