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  4862  f1prex  7232  fliftfun  7260  fprresex  8254  nnaordex2  8569  naddssim  8615  mapdom2  9080  domunfican  9226  fofinf1o  9236  finsschain  9263  wemaplem3  9457  oemapvali  9597  iunfictbso  10028  enfin2i  10235  fin1a2s  10328  distrlem4pr  10941  mulcmpblnr  10986  prsrlem1  10987  addsrmo  10988  mulsrmo  10989  divdivdiv  11846  divsubdiv  11861  lediv12a  12039  xralrple  13124  seqcaopr  13966  leexp2r  14101  hashbclem  14379  wrd2ind  14650  cshwidxmod  14730  rtrclreclem4  14988  relexpindlem  14990  rtrclind  14992  rlimresb  15492  summo  15644  fsum2dlem  15697  prodmo  15863  fprod2dlem  15907  bezoutlem3  16472  bezoutlem4  16473  qredeu  16589  coprmproddvdslem  16593  prmdvdsncoprmbd  16658  pcqmul  16785  pcadd  16821  pockthg  16838  ramub1lem2  16959  cshwsdisj  17030  mreexexlem4d  17574  issubc3  17777  cofucl  17816  setcmon  18015  setcepi  18016  drsdirfi  18232  poslubmo  18336  posglbmo  18337  grprida  18604  ghmpreima  19171  gaorber  19241  psgnunilem4  19430  psgneu  19439  odcau  19537  pgpssslw  19547  fislw  19558  lsmsubm  19586  efgsfo  19672  pgpfac1  20015  pgpfaclem2  20017  pgpfaclem3  20018  unitgrp  20323  islmodd  20821  lmodprop2d  20879  lsspropd  20973  lbsextlem4  21120  assapropd  21831  evlslem1  22041  mdetunilem8  22567  mdetmul  22571  ppttop  22955  epttop  22957  restbas  23106  iscnp4  23211  cnpco  23215  nrmsep  23305  regsep2  23324  ordthauslem  23331  1stcfb  23393  2ndcctbss  23403  2ndcdisj  23404  2ndcomap  23406  dis2ndc  23408  1stcelcls  23409  nlly2i  23424  islly2  23432  hausllycmp  23442  lly1stc  23444  comppfsc  23480  1stckgenlem  23501  ptbasin  23525  txcls  23552  ptcnp  23570  txlly  23584  txnlly  23585  txtube  23588  txcmplem1  23589  txcmplem2  23590  xkococnlem  23607  basqtop  23659  regr1lem  23687  kqreglem1  23689  kqreglem2  23690  kqnrmlem1  23691  kqnrmlem2  23692  reghmph  23741  nrmhmph  23742  filuni  23833  rnelfmlem  23900  fmufil  23907  fclscf  23973  fclsfnflim  23975  flimfnfcls  23976  uffclsflim  23979  cnpfcfi  23988  cnpfcf  23989  alexsublem  23992  alexsubALTlem3  23997  tgpconncompeqg  24060  ghmcnp  24063  qustgplem  24069  blssps  24372  blss  24373  blcld  24453  metequiv2  24458  met2ndci  24470  prdsxmslem2  24477  txmetcnp  24495  nlmvscnlem1  24634  xrge0tsms  24783  ipcnlem1  25205  iscmet3  25253  metsscmetcld  25275  minveclem3  25389  pmltpc  25411  ovolscalem2  25475  ovolicc2lem5  25482  ovolicc2  25483  nulmbl2  25497  ioombl1  25523  uniioombllem6  25549  uniioombl  25550  vitalilem3  25571  i1faddlem  25654  mbfmullem  25686  itg2const2  25702  itg2split  25710  lhop2  25980  dvfsumrlim  25998  itgsubst  26016  plydivex  26265  plyexmo  26281  ulmbdd  26367  cxploglim  26948  dchrptlem2  27236  lgsquad2lem2  27356  2sqlem5  27393  dchrvmasumif  27474  rpvmasum2  27483  dchrisum0re  27484  dchrisum0lem3  27490  dchrisum0  27491  dchrmusum  27495  dchrvmasum  27496  pntibndlem3  27563  pntlemp  27581  ostth3  27609  nosupbday  27677  nosupbnd1lem1  27680  nosupbnd2  27688  noinfbday  27692  noinfbnd1lem1  27695  noinfbnd2  27703  conway  27777  madebdaylemlrcut  27881  mulsproplem9  28106  mulsuniflem  28131  uzsind  28384  bdayfinbndlem1  28446  readdscl  28478  legtrid  28646  hlcgreu  28673  mirreu3  28709  opphllem  28790  oppperpex  28808  lnperpex  28858  trgcopy  28859  iscgra1  28865  cgraswap  28875  cgracom  28877  cgratr  28878  flatcgra  28879  acopyeu  28889  ax5seglem9  28993  ax5seg  28994  axcontlem8  29027  axcontlem12  29031  upgrclwlkcompim  29837  wwlksnextwrd  29953  2pthfrgr  30342  frgrnbnb  30351  ablo4  30608  smcnlem  30755  pjhthmo  31360  1stpreimas  32766  xrge0tsmsd  33136  locfinref  33979  xpinpreima2  34045  qqhval2  34120  dya2iocnrect  34419  orvcgteel  34606  orvclteel  34611  cnpconn  35405  txpconn  35407  connpconn  35410  pconnpi1  35412  iccllysconn  35425  rellysconn  35426  cvmcov2  35450  cvmliftmolem2  35457  cvmliftmo  35459  cvmliftlem15  35473  cvmliftpht  35493  cvmlift3lem2  35495  cgrextend  36183  btwnouttr2  36197  btwnexch2  36198  cgrxfr  36230  lineext  36251  btwnconn1lem5  36266  btwnconn1lem13  36274  btwnconn3  36278  segletr  36289  segleantisym  36290  outsideofeq  36305  outsidele  36307  lineunray  36322  refssfne  36533  neibastop2lem  36535  neibastop2  36536  weiunpo  36640  unblimceq0lem  36681  knoppndvlem22  36708  mblfinlem3  37831  mblfinlem4  37832  cnambfre  37840  itg2addnclem  37843  areacirclem5  37884  istotbnd3  37943  crngm4  38175  cvlcvr1  39636  4atlem12  39909  cdlemb  40091  paddasslem10  40126  paddasslem12  40128  paddasslem13  40129  lhpexle3lem  40308  cdlemd4  40498  cdlemefs32sn1aw  40711  cdleme43fsv1snlem  40717  cdleme32d  40741  cdleme32f  40743  cdleme40m  40764  cdleme40n  40765  cdleme50trn2  40848  cdlemftr3  40862  cdlemm10N  41415  dihvalcqpre  41532  dihopelvalcpre  41545  dihmeetlem1N  41587  dihglblem5apreN  41588  dihmeetlem4preN  41603  dihjat1lem  41725  mapd0  41962  mapdh9a  42086  nna4b4nsq  42939  mzpmfp  43025  mzpcompact2lem  43029  diophin  43050  pellexlem3  43109  pellex  43113  pell14qrmulcl  43141  jm2.19lem3  43269  jm2.25  43277  jm2.27b  43284  fnwe2lem2  43329  hbtlem2  43402  hbtlem5  43406  gsumws3  44473  gsumws4  44474  mnuprdlem1  44549  mnuprdlem2  44550  mnuprdlem4  44552  fnchoice  45310  stoweidlem53  46333  stoweidlem61  46341  qndenserrnbllem  46574  bgoldbtbnd  48091  cycldlenngric  48210  grtrimap  48230  isubgr3stgrlem6  48253  prsthinc  49745