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 730	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  4849  f1prex  7239  fliftfun  7267  fprresex  8260  nnaordex2  8575  naddssim  8621  mapdom2  9086  domunfican  9232  fofinf1o  9242  finsschain  9269  wemaplem3  9463  oemapvali  9605  iunfictbso  10036  enfin2i  10243  fin1a2s  10336  distrlem4pr  10949  mulcmpblnr  10994  prsrlem1  10995  addsrmo  10996  mulsrmo  10997  divdivdiv  11856  divsubdiv  11871  lediv12a  12049  xralrple  13157  seqcaopr  14001  leexp2r  14136  hashbclem  14414  wrd2ind  14685  cshwidxmod  14765  rtrclreclem4  15023  relexpindlem  15025  rtrclind  15027  rlimresb  15527  summo  15679  fsum2dlem  15732  prodmo  15901  fprod2dlem  15945  bezoutlem3  16510  bezoutlem4  16511  qredeu  16627  coprmproddvdslem  16631  prmdvdsncoprmbd  16697  pcqmul  16824  pcadd  16860  pockthg  16877  ramub1lem2  16998  cshwsdisj  17069  mreexexlem4d  17613  issubc3  17816  cofucl  17855  setcmon  18054  setcepi  18055  drsdirfi  18271  poslubmo  18375  posglbmo  18376  grprida  18643  ghmpreima  19213  gaorber  19283  psgnunilem4  19472  psgneu  19481  odcau  19579  pgpssslw  19589  fislw  19600  lsmsubm  19628  efgsfo  19714  pgpfac1  20057  pgpfaclem2  20059  pgpfaclem3  20060  unitgrp  20363  islmodd  20861  lmodprop2d  20919  lsspropd  21012  lbsextlem4  21159  assapropd  21851  evlslem1  22060  mdetunilem8  22584  mdetmul  22588  ppttop  22972  epttop  22974  restbas  23123  iscnp4  23228  cnpco  23232  nrmsep  23322  regsep2  23341  ordthauslem  23348  1stcfb  23410  2ndcctbss  23420  2ndcdisj  23421  2ndcomap  23423  dis2ndc  23425  1stcelcls  23426  nlly2i  23441  islly2  23449  hausllycmp  23459  lly1stc  23461  comppfsc  23497  1stckgenlem  23518  ptbasin  23542  txcls  23569  ptcnp  23587  txlly  23601  txnlly  23602  txtube  23605  txcmplem1  23606  txcmplem2  23607  xkococnlem  23624  basqtop  23676  regr1lem  23704  kqreglem1  23706  kqreglem2  23707  kqnrmlem1  23708  kqnrmlem2  23709  reghmph  23758  nrmhmph  23759  filuni  23850  rnelfmlem  23917  fmufil  23924  fclscf  23990  fclsfnflim  23992  flimfnfcls  23993  uffclsflim  23996  cnpfcfi  24005  cnpfcf  24006  alexsublem  24009  alexsubALTlem3  24014  tgpconncompeqg  24077  ghmcnp  24080  qustgplem  24086  blssps  24389  blss  24390  blcld  24470  metequiv2  24475  met2ndci  24487  prdsxmslem2  24494  txmetcnp  24512  nlmvscnlem1  24651  xrge0tsms  24800  ipcnlem1  25212  iscmet3  25260  metsscmetcld  25282  minveclem3  25396  pmltpc  25417  ovolscalem2  25481  ovolicc2lem5  25488  ovolicc2  25489  nulmbl2  25503  ioombl1  25529  uniioombllem6  25555  uniioombl  25556  vitalilem3  25577  i1faddlem  25660  mbfmullem  25692  itg2const2  25708  itg2split  25716  lhop2  25982  dvfsumrlim  25998  itgsubst  26016  plydivex  26263  plyexmo  26279  ulmbdd  26363  cxploglim  26941  dchrptlem2  27228  lgsquad2lem2  27348  2sqlem5  27385  dchrvmasumif  27466  rpvmasum2  27475  dchrisum0re  27476  dchrisum0lem3  27482  dchrisum0  27483  dchrmusum  27487  dchrvmasum  27488  pntibndlem3  27555  pntlemp  27573  ostth3  27601  nosupbday  27669  nosupbnd1lem1  27672  nosupbnd2  27680  noinfbday  27684  noinfbnd1lem1  27687  noinfbnd2  27695  conway  27771  madebdaylemlrcut  27891  mulsproplem9  28116  mulsuniflem  28141  uzsind  28397  bdayfinbndlem1  28459  readdscl  28491  legtrid  28659  hlcgreu  28686  mirreu3  28722  opphllem  28803  oppperpex  28821  lnperpex  28871  trgcopy  28872  iscgra1  28878  cgraswap  28888  cgracom  28890  cgratr  28891  flatcgra  28892  acopyeu  28902  ax5seglem9  29006  ax5seg  29007  axcontlem8  29040  axcontlem12  29044  upgrclwlkcompim  29849  wwlksnextwrd  29965  2pthfrgr  30354  frgrnbnb  30363  ablo4  30621  smcnlem  30768  pjhthmo  31373  1stpreimas  32779  xrge0tsmsd  33134  locfinref  33985  xpinpreima2  34051  qqhval2  34126  dya2iocnrect  34425  orvcgteel  34612  orvclteel  34617  cnpconn  35412  txpconn  35414  connpconn  35417  pconnpi1  35419  iccllysconn  35432  rellysconn  35433  cvmcov2  35457  cvmliftmolem2  35464  cvmliftmo  35466  cvmliftlem15  35480  cvmliftpht  35500  cvmlift3lem2  35502  cgrextend  36190  btwnouttr2  36204  btwnexch2  36205  cgrxfr  36237  lineext  36258  btwnconn1lem5  36273  btwnconn1lem13  36281  btwnconn3  36285  segletr  36296  segleantisym  36297  outsideofeq  36312  outsidele  36314  lineunray  36329  refssfne  36540  neibastop2lem  36542  neibastop2  36543  weiunpo  36647  unblimceq0lem  36766  knoppndvlem22  36793  mblfinlem3  37980  mblfinlem4  37981  cnambfre  37989  itg2addnclem  37992  areacirclem5  38033  istotbnd3  38092  crngm4  38324  cvlcvr1  39785  4atlem12  40058  cdlemb  40240  paddasslem10  40275  paddasslem12  40277  paddasslem13  40278  lhpexle3lem  40457  cdlemd4  40647  cdlemefs32sn1aw  40860  cdleme43fsv1snlem  40866  cdleme32d  40890  cdleme32f  40892  cdleme40m  40913  cdleme40n  40914  cdleme50trn2  40997  cdlemftr3  41011  cdlemm10N  41564  dihvalcqpre  41681  dihopelvalcpre  41694  dihmeetlem1N  41736  dihglblem5apreN  41737  dihmeetlem4preN  41752  dihjat1lem  41874  mapd0  42111  mapdh9a  42235  nna4b4nsq  43093  mzpmfp  43179  mzpcompact2lem  43183  diophin  43204  pellexlem3  43259  pellex  43263  pell14qrmulcl  43291  jm2.19lem3  43419  jm2.25  43427  jm2.27b  43434  fnwe2lem2  43479  hbtlem2  43552  hbtlem5  43556  gsumws3  44623  gsumws4  44624  mnuprdlem1  44699  mnuprdlem2  44700  mnuprdlem4  44702  fnchoice  45460  stoweidlem53  46481  stoweidlem61  46489  qndenserrnbllem  46722  bgoldbtbnd  48279  cycldlenngric  48398  grtrimap  48418  isubgr3stgrlem6  48441  prsthinc  49933