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 728	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  4901  f1prex  7287  fliftfun  7314  fprresex  8309  wfrlem17OLD  8339  nnaordex2  8653  naddssim  8699  mapdom2  9164  domunfican  9336  fofinf1o  9343  finsschain  9375  wemaplem3  9563  oemapvali  9699  iunfictbso  10129  enfin2i  10336  fin1a2s  10429  distrlem4pr  11041  mulcmpblnr  11086  prsrlem1  11087  addsrmo  11088  mulsrmo  11089  divdivdiv  11937  divsubdiv  11952  lediv12a  12129  xralrple  13208  seqcaopr  14028  leexp2r  14162  hashbclem  14435  wrd2ind  14697  cshwidxmod  14777  rtrclreclem4  15032  relexpindlem  15034  rtrclind  15036  rlimresb  15533  summo  15687  fsum2dlem  15740  prodmo  15904  fprod2dlem  15948  bezoutlem3  16508  bezoutlem4  16509  qredeu  16620  coprmproddvdslem  16624  prmdvdsncoprmbd  16690  pcqmul  16813  pcadd  16849  pockthg  16866  ramub1lem2  16987  cshwsdisj  17059  mreexexlem4d  17618  issubc3  17826  cofucl  17865  setcmon  18067  setcepi  18068  drsdirfi  18288  poslubmo  18394  posglbmo  18395  grprida  18626  ghmpreima  19183  gaorber  19250  psgnunilem4  19443  psgneu  19452  odcau  19550  pgpssslw  19560  fislw  19571  lsmsubm  19599  efgsfo  19685  pgpfac1  20028  pgpfaclem2  20030  pgpfaclem3  20031  unitgrp  20311  islmodd  20738  lmodprop2d  20796  lsspropd  20891  lbsextlem4  21038  assapropd  21792  evlslem1  22015  mdetunilem8  22508  mdetmul  22512  ppttop  22897  epttop  22899  restbas  23049  iscnp4  23154  cnpco  23158  nrmsep  23248  regsep2  23267  ordthauslem  23274  1stcfb  23336  2ndcctbss  23346  2ndcdisj  23347  2ndcomap  23349  dis2ndc  23351  1stcelcls  23352  nlly2i  23367  islly2  23375  hausllycmp  23385  lly1stc  23387  comppfsc  23423  1stckgenlem  23444  ptbasin  23468  txcls  23495  ptcnp  23513  txlly  23527  txnlly  23528  txtube  23531  txcmplem1  23532  txcmplem2  23533  xkococnlem  23550  basqtop  23602  regr1lem  23630  kqreglem1  23632  kqreglem2  23633  kqnrmlem1  23634  kqnrmlem2  23635  reghmph  23684  nrmhmph  23685  filuni  23776  rnelfmlem  23843  fmufil  23850  fclscf  23916  fclsfnflim  23918  flimfnfcls  23919  uffclsflim  23922  cnpfcfi  23931  cnpfcf  23932  alexsublem  23935  alexsubALTlem3  23940  tgpconncompeqg  24003  ghmcnp  24006  qustgplem  24012  blssps  24317  blss  24318  blcld  24401  metequiv2  24406  met2ndci  24418  prdsxmslem2  24425  txmetcnp  24443  nlmvscnlem1  24590  xrge0tsms  24737  ipcnlem1  25160  iscmet3  25208  metsscmetcld  25230  minveclem3  25344  pmltpc  25366  ovolscalem2  25430  ovolicc2lem5  25437  ovolicc2  25438  nulmbl2  25452  ioombl1  25478  uniioombllem6  25504  uniioombl  25505  vitalilem3  25526  i1faddlem  25609  mbfmullem  25642  itg2const2  25658  itg2split  25666  lhop2  25935  dvfsumrlim  25953  itgsubst  25971  plydivex  26219  plyexmo  26235  ulmbdd  26321  cxploglim  26897  dchrptlem2  27185  lgsquad2lem2  27305  2sqlem5  27342  dchrvmasumif  27423  rpvmasum2  27432  dchrisum0re  27433  dchrisum0lem3  27439  dchrisum0  27440  dchrmusum  27444  dchrvmasum  27445  pntibndlem3  27512  pntlemp  27530  ostth3  27558  nosupbday  27625  nosupbnd1lem1  27628  nosupbnd2  27636  noinfbday  27640  noinfbnd1lem1  27643  noinfbnd2  27651  conway  27719  madebdaylemlrcut  27812  mulsproplem9  28011  mulsuniflem  28036  readdscl  28214  legtrid  28382  hlcgreu  28409  mirreu3  28445  opphllem  28526  oppperpex  28544  lnperpex  28594  trgcopy  28595  iscgra1  28601  cgraswap  28611  cgracom  28613  cgratr  28614  flatcgra  28615  acopyeu  28625  ax5seglem9  28735  ax5seg  28736  axcontlem8  28769  axcontlem12  28773  upgrclwlkcompim  29582  wwlksnextwrd  29695  2pthfrgr  30081  frgrnbnb  30090  ablo4  30347  smcnlem  30494  pjhthmo  31099  1stpreimas  32469  xrge0tsmsd  32749  locfinref  33378  xpinpreima2  33444  qqhval2  33519  dya2iocnrect  33837  orvcgteel  34023  orvclteel  34028  cnpconn  34776  txpconn  34778  connpconn  34781  pconnpi1  34783  iccllysconn  34796  rellysconn  34797  cvmcov2  34821  cvmliftmolem2  34828  cvmliftmo  34830  cvmliftlem15  34844  cvmliftpht  34864  cvmlift3lem2  34866  cgrextend  35540  btwnouttr2  35554  btwnexch2  35555  cgrxfr  35587  lineext  35608  btwnconn1lem5  35623  btwnconn1lem13  35631  btwnconn3  35635  segletr  35646  segleantisym  35647  outsideofeq  35662  outsidele  35664  lineunray  35679  refssfne  35778  neibastop2lem  35780  neibastop2  35781  unblimceq0lem  35917  knoppndvlem22  35944  mblfinlem3  37067  mblfinlem4  37068  cnambfre  37076  itg2addnclem  37079  areacirclem5  37120  istotbnd3  37179  crngm4  37411  cvlcvr1  38748  4atlem12  39022  cdlemb  39204  paddasslem10  39239  paddasslem12  39241  paddasslem13  39242  lhpexle3lem  39421  cdlemd4  39611  cdlemefs32sn1aw  39824  cdleme43fsv1snlem  39830  cdleme32d  39854  cdleme32f  39856  cdleme40m  39877  cdleme40n  39878  cdleme50trn2  39961  cdlemftr3  39975  cdlemm10N  40528  dihvalcqpre  40645  dihopelvalcpre  40658  dihmeetlem1N  40700  dihglblem5apreN  40701  dihmeetlem4preN  40716  dihjat1lem  40838  mapd0  41075  mapdh9a  41199  nna4b4nsq  42006  mzpmfp  42089  mzpcompact2lem  42093  diophin  42114  pellexlem3  42173  pellex  42177  pell14qrmulcl  42205  jm2.19lem3  42334  jm2.25  42342  jm2.27b  42349  fnwe2lem2  42397  hbtlem2  42470  hbtlem5  42474  gsumws3  43549  gsumws4  43550  mnuprdlem1  43632  mnuprdlem2  43633  mnuprdlem4  43635  fnchoice  44314  stoweidlem53  45364  stoweidlem61  45372  qndenserrnbllem  45605  bgoldbtbnd  47072  prsthinc  47983