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 483	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜃)
2	1	ad2antll 725	1 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  prproe  4905  f1prex  7284  fliftfun  7311  fprresex  8297  wfrlem17OLD  8327  naddssim  8686  mapdom2  9150  domunfican  9322  fofinf1o  9329  finsschain  9361  wemaplem3  9545  oemapvali  9681  iunfictbso  10111  enfin2i  10318  fin1a2s  10411  distrlem4pr  11023  mulcmpblnr  11068  prsrlem1  11069  addsrmo  11070  mulsrmo  11071  divdivdiv  11919  divsubdiv  11934  lediv12a  12111  xralrple  13188  seqcaopr  14009  leexp2r  14143  hashbclem  14415  wrd2ind  14677  cshwidxmod  14757  rtrclreclem4  15012  relexpindlem  15014  rtrclind  15016  rlimresb  15513  summo  15667  fsum2dlem  15720  prodmo  15884  fprod2dlem  15928  bezoutlem3  16487  bezoutlem4  16488  qredeu  16599  coprmproddvdslem  16603  prmdvdsncoprmbd  16667  pcqmul  16790  pcadd  16826  pockthg  16843  ramub1lem2  16964  cshwsdisj  17036  mreexexlem4d  17595  issubc3  17803  cofucl  17842  setcmon  18041  setcepi  18042  drsdirfi  18262  poslubmo  18368  posglbmo  18369  grprida  18600  ghmpreima  19152  gaorber  19213  psgnunilem4  19406  psgneu  19415  odcau  19513  pgpssslw  19523  fislw  19534  lsmsubm  19562  efgsfo  19648  pgpfac1  19991  pgpfaclem2  19993  pgpfaclem3  19994  unitgrp  20274  islmodd  20620  lmodprop2d  20678  lsspropd  20772  lbsextlem4  20919  assapropd  21645  evlslem1  21864  mdetunilem8  22341  mdetmul  22345  ppttop  22730  epttop  22732  restbas  22882  iscnp4  22987  cnpco  22991  nrmsep  23081  regsep2  23100  ordthauslem  23107  1stcfb  23169  2ndcctbss  23179  2ndcdisj  23180  2ndcomap  23182  dis2ndc  23184  1stcelcls  23185  nlly2i  23200  islly2  23208  hausllycmp  23218  lly1stc  23220  comppfsc  23256  1stckgenlem  23277  ptbasin  23301  txcls  23328  ptcnp  23346  txlly  23360  txnlly  23361  txtube  23364  txcmplem1  23365  txcmplem2  23366  xkococnlem  23383  basqtop  23435  regr1lem  23463  kqreglem1  23465  kqreglem2  23466  kqnrmlem1  23467  kqnrmlem2  23468  reghmph  23517  nrmhmph  23518  filuni  23609  rnelfmlem  23676  fmufil  23683  fclscf  23749  fclsfnflim  23751  flimfnfcls  23752  uffclsflim  23755  cnpfcfi  23764  cnpfcf  23765  alexsublem  23768  alexsubALTlem3  23773  tgpconncompeqg  23836  ghmcnp  23839  qustgplem  23845  blssps  24150  blss  24151  blcld  24234  metequiv2  24239  met2ndci  24251  prdsxmslem2  24258  txmetcnp  24276  nlmvscnlem1  24423  xrge0tsms  24570  ipcnlem1  24993  iscmet3  25041  metsscmetcld  25063  minveclem3  25177  pmltpc  25199  ovolscalem2  25263  ovolicc2lem5  25270  ovolicc2  25271  nulmbl2  25285  ioombl1  25311  uniioombllem6  25337  uniioombl  25338  vitalilem3  25359  i1faddlem  25442  mbfmullem  25475  itg2const2  25491  itg2split  25499  lhop2  25767  dvfsumrlim  25783  itgsubst  25801  plydivex  26046  plyexmo  26062  ulmbdd  26146  cxploglim  26718  dchrptlem2  27004  lgsquad2lem2  27124  2sqlem5  27161  dchrvmasumif  27242  rpvmasum2  27251  dchrisum0re  27252  dchrisum0lem3  27258  dchrisum0  27259  dchrmusum  27263  dchrvmasum  27264  pntibndlem3  27331  pntlemp  27349  ostth3  27377  nosupbday  27444  nosupbnd1lem1  27447  nosupbnd2  27455  noinfbday  27459  noinfbnd1lem1  27462  noinfbnd2  27470  conway  27537  madebdaylemlrcut  27630  mulsproplem9  27819  mulsuniflem  27843  legtrid  28109  hlcgreu  28136  mirreu3  28172  opphllem  28253  oppperpex  28271  lnperpex  28321  trgcopy  28322  iscgra1  28328  cgraswap  28338  cgracom  28340  cgratr  28341  flatcgra  28342  acopyeu  28352  ax5seglem9  28462  ax5seg  28463  axcontlem8  28496  axcontlem12  28500  upgrclwlkcompim  29305  wwlksnextwrd  29418  2pthfrgr  29804  frgrnbnb  29813  ablo4  30070  smcnlem  30217  pjhthmo  30822  1stpreimas  32194  xrge0tsmsd  32479  locfinref  33119  xpinpreima2  33185  qqhval2  33260  dya2iocnrect  33578  orvcgteel  33764  orvclteel  33769  cnpconn  34519  txpconn  34521  connpconn  34524  pconnpi1  34526  iccllysconn  34539  rellysconn  34540  cvmcov2  34564  cvmliftmolem2  34571  cvmliftmo  34573  cvmliftlem15  34587  cvmliftpht  34607  cvmlift3lem2  34609  cgrextend  35284  btwnouttr2  35298  btwnexch2  35299  cgrxfr  35331  lineext  35352  btwnconn1lem5  35367  btwnconn1lem13  35375  btwnconn3  35379  segletr  35390  segleantisym  35391  outsideofeq  35406  outsidele  35408  lineunray  35423  refssfne  35546  neibastop2lem  35548  neibastop2  35549  unblimceq0lem  35685  knoppndvlem22  35712  mblfinlem3  36830  mblfinlem4  36831  cnambfre  36839  itg2addnclem  36842  areacirclem5  36883  istotbnd3  36942  crngm4  37174  cvlcvr1  38512  4atlem12  38786  cdlemb  38968  paddasslem10  39003  paddasslem12  39005  paddasslem13  39006  lhpexle3lem  39185  cdlemd4  39375  cdlemefs32sn1aw  39588  cdleme43fsv1snlem  39594  cdleme32d  39618  cdleme32f  39620  cdleme40m  39641  cdleme40n  39642  cdleme50trn2  39725  cdlemftr3  39739  cdlemm10N  40292  dihvalcqpre  40409  dihopelvalcpre  40422  dihmeetlem1N  40464  dihglblem5apreN  40465  dihmeetlem4preN  40480  dihjat1lem  40602  mapd0  40839  mapdh9a  40963  nna4b4nsq  41704  mzpmfp  41787  mzpcompact2lem  41791  diophin  41812  pellexlem3  41871  pellex  41875  pell14qrmulcl  41903  jm2.19lem3  42032  jm2.25  42040  jm2.27b  42047  fnwe2lem2  42095  hbtlem2  42168  hbtlem5  42172  gsumws3  43250  gsumws4  43251  mnuprdlem1  43333  mnuprdlem2  43334  mnuprdlem4  43336  fnchoice  44015  stoweidlem53  45067  stoweidlem61  45075  qndenserrnbllem  45308  bgoldbtbnd  46775  prsthinc  47761