Theorem simprrr 794

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  prproe  4864  f1prex  7292  fliftfun  7320  fnwe2lem3  8147  fprresex  8328  nnaordex2  8648  naddssim  8695  mapdom2  9167  domunfican  9313  fofinf1o  9321  finsschain  9348  wemaplem3  9542  oemapvali  9685  iunfictbso  10193  enfin2i  10399  fin1a2s  10492  distrlem4pr  11111  mulcmpblnr  11156  prsrlem1  11157  addsrmo  11158  mulsrmo  11159  divdivdiv  12018  divsubdiv  12033  lediv12a  12210  xralrple  13335  seqcaopr  14182  leexp2r  14317  hashbclem  14597  wrd2ind  14872  cshwidxmod  14954  rtrclreclem4  15214  relexpindlem  15216  rtrclind  15218  rlimresb  15732  summo  15883  fsum2dlem  15936  prodmo  16103  fprod2dlem  16147  bezoutlem3  16714  bezoutlem4  16715  qredeu  16833  coprmproddvdslem  16837  prmdvdsncoprmbd  16903  pcqmul  17031  pcadd  17067  pockthg  17084  ramub1lem2  17205  cshwsdisj  17276  mreexexlem4d  17821  issubc3  18024  cofucl  18063  setcmon  18262  setcepi  18263  drsdirfi  18479  poslubmo  18583  posglbmo  18584  mgmn0plusgf  18827  grprida  18856  ghmpreima  19452  gaorber  19522  psgnunilem4  19711  psgneu  19720  odcau  19818  pgpssslw  19828  fislw  19839  lsmsubm  19867  efgsfo  19953  pgpfac1  20296  pgpfaclem2  20298  pgpfaclem3  20299  unitgrp  20613  islmodd  21141  lmodprop2d  21199  lsspropd  21292  lbsextlem4  21439  assapropd  22179  evlslem1  22391  mdetunilem8  22934  mdetmul  22938  ppttop  23325  epttop  23327  restbas  23476  iscnp4  23581  cnpco  23585  nrmsep  23675  regsep2  23694  ordthauslem  23701  1stcfb  23763  2ndcctbss  23774  2ndcdisj  23775  2ndcomap  23777  dis2ndc  23779  1stcelcls  23780  nlly2i  23795  islly2  23803  hausllycmp  23813  lly1stc  23815  comppfsc  23851  1stckgenlem  23872  ptbasin  23896  txcls  23923  ptcnp  23941  txlly  23955  txnlly  23956  txtube  23959  txcmplem1  23960  txcmplem2  23961  xkococnlem  23978  basqtop  24030  regr1lem  24058  kqreglem1  24060  kqreglem2  24061  kqnrmlem1  24062  kqnrmlem2  24063  reghmph  24112  nrmhmph  24113  filuni  24204  rnelfmlem  24271  fmufil  24278  fclscf  24344  fclsfnflim  24346  flimfnfcls  24347  uffclsflim  24350  cnpfcfi  24359  cnpfcf  24360  alexsublem  24363  alexsubALTlem3  24368  tgpconncompeqg  24431  ghmcnp  24434  qustgplem  24440  blssps  24743  blss  24744  blcld  24824  metequiv2  24829  met2ndci  24841  prdsxmslem2  24848  txmetcnp  24866  nlmvscnlem1  25005  xrge0tsms  25154  ipcnlem1  25566  iscmet3  25614  metsscmetcld  25636  minveclem3  25750  pmltpc  25771  ovolscalem2  25835  ovolicc2lem5  25842  ovolicc2  25843  nulmbl2  25857  ioombl1  25883  uniioombllem6  25909  uniioombl  25910  vitalilem3  25931  i1faddlem  26014  mbfmullem  26046  itg2const2  26062  itg2split  26070  lhop2  26335  dvfsumrlim  26351  itgsubst  26369  plydivex  26618  plyexmo  26636  ulmbdd  26725  cxploglim  27305  dchrptlem2  27592  lgsquad2lem2  27712  2sqlem5  27749  dchrvmasumif  27830  rpvmasum2  27839  dchrisum0re  27840  dchrisum0lem3  27846  dchrisum0  27847  dchrmusum  27851  dchrvmasum  27852  pntibndlem3  27919  pntlemp  27937  ostth3  27965  nna4b4nsq  27990  nosupbday  28062  nosupbnd1lem1  28065  nosupbnd2  28073  noinfbday  28077  noinfbnd1lem1  28080  noinfbnd2  28088  conway  28165  madebdaylemlrcut  28285  mulsproplem9  28510  mulsuniflem  28535  uzsind  28791  bdayfinbndlem1  28853  readdscl  28885  legtrid  29054  hlcgreu  29084  mirreu3  29126  opphllem  29211  oppperpex  29229  lnperpex  29309  trgcopy  29311  iscgra1  29317  cgraswap  29327  cgracom  29329  cgratr  29330  flatcgra  29332  acopyeu  29342  ax5seglem9  29515  ax5seg  29516  axcontlem8  29549  axcontlem12  29553  upgrclwlkcompim  30368  wwlksnextwrd  30486  2pthfrgr  30885  frgrnbnb  30894  ablo4  31152  smcnlem  31299  pjhthmo  31904  tgextahp  33073  1stpreimas  33341  xrge0tsmsd  33676  locfinref  34515  xpinpreima2  34581  qqhval2  34656  dya2iocnrect  34955  orvcgteel  35142  orvclteel  35147  cnpconn  36037  txpconn  36039  connpconn  36042  pconnpi1  36044  iccllysconn  36057  rellysconn  36058  cvmcov2  36082  cvmliftmolem2  36089  cvmliftmo  36091  cvmliftlem15  36105  cvmliftpht  36125  cvmlift3lem2  36127  cgrextend  36815  btwnouttr2  36829  btwnexch2  36830  cgrxfr  36862  lineext  36883  btwnconn1lem5  36898  btwnconn1lem13  36906  btwnconn3  36910  segletr  36921  segleantisym  36922  outsideofeq  36937  outsidele  36939  lineunray  36954  refssfne  37188  neibastop2lem  37190  neibastop2  37191  weiunpo  37295  unblimceq0lem  37414  knoppndvlem22  37441  mblfinlem3  38620  mblfinlem4  38621  cnambfre  38629  itg2addnclem  38632  areacirclem5  38673  istotbnd3  38748  crngm4  38980  cvlcvr1  40439  4atlem12  40712  cdlemb  40894  paddasslem10  40929  paddasslem12  40931  paddasslem13  40932  lhpexle3lem  41111  cdlemd4  41301  cdlemefs32sn1aw  41514  cdleme43fsv1snlem  41520  cdleme32d  41544  cdleme32f  41546  cdleme40m  41567  cdleme40n  41568  cdleme50trn2  41651  cdlemftr3  41665  cdlemm10N  42218  dihvalcqpre  42335  dihopelvalcpre  42348  dihmeetlem1N  42390  dihglblem5apreN  42391  dihmeetlem4preN  42406  dihjat1lem  42528  mapd0  42765  mapdh9a  42889  mzpmfp  43801  mzpcompact2lem  43805  diophin  43826  pellexlem3  43881  pellex  43885  pell14qrmulcl  43913  jm2.19lem3  44041  jm2.25  44049  jm2.27b  44056  hbtlem2  44169  hbtlem5  44173  gsumws3  45239  gsumws4  45240  mnuprdlem1  45299  mnuprdlem2  45300  mnuprdlem4  45302  fnchoice  46089  stoweidlem53  47106  stoweidlem61  47114  qndenserrnbllem  47347  bgoldbtbnd  48950  cycldlenngric  49069  grtrimap  49089  isubgr3stgrlem6  49112  prsthinc  50615