Theorem simprrr 778

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 725	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 206  df-an 396

This theorem is referenced by:  prproe  4834  f1prex  7136  fliftfun  7163  fprresex  8097  wfrlem17OLD  8127  mapdom2  8884  domunfican  9017  fofinf1o  9024  finsschain  9056  wemaplem3  9237  oemapvali  9372  iunfictbso  9801  enfin2i  10008  fin1a2s  10101  distrlem4pr  10713  mulcmpblnr  10758  prsrlem1  10759  addsrmo  10760  mulsrmo  10761  divdivdiv  11606  divsubdiv  11621  lediv12a  11798  xralrple  12868  seqcaopr  13688  leexp2r  13820  hashbclem  14092  wrd2ind  14364  cshwidxmod  14444  rtrclreclem4  14700  relexpindlem  14702  rtrclind  14704  rlimresb  15202  summo  15357  fsum2dlem  15410  prodmo  15574  fprod2dlem  15618  bezoutlem3  16177  bezoutlem4  16178  qredeu  16291  coprmproddvdslem  16295  prmdvdsncoprmbd  16359  pcqmul  16482  pcadd  16518  pockthg  16535  ramub1lem2  16656  cshwsdisj  16728  mreexexlem4d  17273  issubc3  17480  cofucl  17519  setcmon  17718  setcepi  17719  drsdirfi  17938  poslubmo  18044  posglbmo  18045  grpridd  18274  ghmpreima  18771  gaorber  18829  psgnunilem4  19020  psgneu  19029  odcau  19124  pgpssslw  19134  fislw  19145  lsmsubm  19173  efgsfo  19260  pgpfac1  19598  pgpfaclem2  19600  pgpfaclem3  19601  unitgrp  19824  islmodd  20044  lmodprop2d  20100  lsspropd  20194  lbsextlem4  20338  assapropd  20986  evlslem1  21202  mdetunilem8  21676  mdetmul  21680  ppttop  22065  epttop  22067  restbas  22217  iscnp4  22322  cnpco  22326  nrmsep  22416  regsep2  22435  ordthauslem  22442  1stcfb  22504  2ndcctbss  22514  2ndcdisj  22515  2ndcomap  22517  dis2ndc  22519  1stcelcls  22520  nlly2i  22535  islly2  22543  hausllycmp  22553  lly1stc  22555  comppfsc  22591  1stckgenlem  22612  ptbasin  22636  txcls  22663  ptcnp  22681  txlly  22695  txnlly  22696  txtube  22699  txcmplem1  22700  txcmplem2  22701  xkococnlem  22718  basqtop  22770  regr1lem  22798  kqreglem1  22800  kqreglem2  22801  kqnrmlem1  22802  kqnrmlem2  22803  reghmph  22852  nrmhmph  22853  filuni  22944  rnelfmlem  23011  fmufil  23018  fclscf  23084  fclsfnflim  23086  flimfnfcls  23087  uffclsflim  23090  cnpfcfi  23099  cnpfcf  23100  alexsublem  23103  alexsubALTlem3  23108  tgpconncompeqg  23171  ghmcnp  23174  qustgplem  23180  blssps  23485  blss  23486  blcld  23567  metequiv2  23572  met2ndci  23584  prdsxmslem2  23591  txmetcnp  23609  nlmvscnlem1  23756  xrge0tsms  23903  ipcnlem1  24314  iscmet3  24362  metsscmetcld  24384  minveclem3  24498  pmltpc  24519  ovolscalem2  24583  ovolicc2lem5  24590  ovolicc2  24591  nulmbl2  24605  ioombl1  24631  uniioombllem6  24657  uniioombl  24658  vitalilem3  24679  i1faddlem  24762  mbfmullem  24795  itg2const2  24811  itg2split  24819  lhop2  25084  dvfsumrlim  25100  itgsubst  25118  plydivex  25362  plyexmo  25378  ulmbdd  25462  cxploglim  26032  dchrptlem2  26318  lgsquad2lem2  26438  2sqlem5  26475  dchrvmasumif  26556  rpvmasum2  26565  dchrisum0re  26566  dchrisum0lem3  26572  dchrisum0  26573  dchrmusum  26577  dchrvmasum  26578  pntibndlem3  26645  pntlemp  26663  ostth3  26691  legtrid  26856  hlcgreu  26883  mirreu3  26919  opphllem  27000  oppperpex  27018  lnperpex  27068  trgcopy  27069  iscgra1  27075  cgraswap  27085  cgracom  27087  cgratr  27088  flatcgra  27089  acopyeu  27099  ax5seglem9  27208  ax5seg  27209  axcontlem8  27242  axcontlem12  27246  upgrclwlkcompim  28050  wwlksnextwrd  28163  2pthfrgr  28549  frgrnbnb  28558  ablo4  28813  smcnlem  28960  pjhthmo  29565  1stpreimas  30940  xrge0tsmsd  31219  locfinref  31693  xpinpreima2  31759  qqhval2  31832  dya2iocnrect  32148  orvcgteel  32334  orvclteel  32339  cnpconn  33092  txpconn  33094  connpconn  33097  pconnpi1  33099  iccllysconn  33112  rellysconn  33113  cvmcov2  33137  cvmliftmolem2  33144  cvmliftmo  33146  cvmliftlem15  33160  cvmliftpht  33180  cvmlift3lem2  33182  naddssim  33764  nosupbday  33835  nosupbnd1lem1  33838  nosupbnd2  33846  noinfbday  33850  noinfbnd1lem1  33853  noinfbnd2  33861  conway  33920  madebdaylemlrcut  34006  cgrextend  34237  btwnouttr2  34251  btwnexch2  34252  cgrxfr  34284  lineext  34305  btwnconn1lem5  34320  btwnconn1lem13  34328  btwnconn3  34332  segletr  34343  segleantisym  34344  outsideofeq  34359  outsidele  34361  lineunray  34376  refssfne  34474  neibastop2lem  34476  neibastop2  34477  unblimceq0lem  34613  knoppndvlem22  34640  mblfinlem3  35743  mblfinlem4  35744  cnambfre  35752  itg2addnclem  35755  areacirclem5  35796  istotbnd3  35856  crngm4  36088  cvlcvr1  37280  4atlem12  37553  cdlemb  37735  paddasslem10  37770  paddasslem12  37772  paddasslem13  37773  lhpexle3lem  37952  cdlemd4  38142  cdlemefs32sn1aw  38355  cdleme43fsv1snlem  38361  cdleme32d  38385  cdleme32f  38387  cdleme40m  38408  cdleme40n  38409  cdleme50trn2  38492  cdlemftr3  38506  cdlemm10N  39059  dihvalcqpre  39176  dihopelvalcpre  39189  dihmeetlem1N  39231  dihglblem5apreN  39232  dihmeetlem4preN  39247  dihjat1lem  39369  mapd0  39606  mapdh9a  39730  nna4b4nsq  40413  mzpmfp  40485  mzpcompact2lem  40489  diophin  40510  pellexlem3  40569  pellex  40573  pell14qrmulcl  40601  jm2.19lem3  40729  jm2.25  40737  jm2.27b  40744  fnwe2lem2  40792  hbtlem2  40865  hbtlem5  40869  gsumws3  41696  gsumws4  41697  mnuprdlem1  41779  mnuprdlem2  41780  mnuprdlem4  41782  fnchoice  42461  stoweidlem53  43484  stoweidlem61  43492  qndenserrnbllem  43725  bgoldbtbnd  45149  prsthinc  46223