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  4836  f1prex  7315  fliftfun  7343  fnwe2lem3  8174  fprresex  8356  nnaordex2  8676  naddssim  8723  mapdom2  9195  domunfican  9341  fofinf1o  9349  finsschain  9376  wemaplem3  9569  oemapvali  9712  iunfictbso  10220  enfin2i  10426  fin1a2s  10519  distrlem4pr  11138  mulcmpblnr  11183  prsrlem1  11184  addsrmo  11185  mulsrmo  11186  divdivdiv  12045  divsubdiv  12060  lediv12a  12237  xralrple  13362  seqcaopr  14209  leexp2r  14344  hashbclem  14624  wrd2ind  14900  cshwidxmod  14982  rtrclreclem4  15243  relexpindlem  15245  rtrclind  15247  rlimresb  15761  summo  15912  fsum2dlem  15965  prodmo  16132  fprod2dlem  16176  bezoutlem3  16743  bezoutlem4  16744  qredeu  16862  coprmproddvdslem  16866  prmdvdsncoprmbd  16932  pcqmul  17060  pcadd  17096  pockthg  17113  ramub1lem2  17234  cshwsdisj  17305  mreexexlem4d  17850  issubc3  18053  cofucl  18092  setcmon  18291  setcepi  18292  drsdirfi  18508  poslubmo  18612  posglbmo  18613  mgmn0plusgf  18856  grprida  18885  ghmpreima  19481  gaorber  19552  psgnunilem4  19741  psgneu  19750  odcau  19848  pgpssslw  19858  fislw  19869  lsmsubm  19897  efgsfo  19983  pgpfac1  20326  pgpfaclem2  20328  pgpfaclem3  20329  unitgrp  20643  islmodd  21171  lmodprop2d  21229  lsspropd  21322  lbsextlem4  21469  assapropd  22209  evlslem1  22421  mdetunilem8  22964  mdetmul  22968  ppttop  23355  epttop  23357  restbas  23506  iscnp4  23611  cnpco  23615  nrmsep  23705  regsep2  23724  ordthauslem  23731  1stcfb  23793  2ndcctbss  23804  2ndcdisj  23805  2ndcomap  23807  dis2ndc  23809  1stcelcls  23810  nlly2i  23825  islly2  23833  hausllycmp  23843  lly1stc  23845  comppfsc  23881  1stckgenlem  23902  ptbasin  23926  txcls  23953  ptcnp  23971  txlly  23985  txnlly  23986  txtube  23989  txcmplem1  23990  txcmplem2  23991  xkococnlem  24008  basqtop  24060  regr1lem  24088  kqreglem1  24090  kqreglem2  24091  kqnrmlem1  24092  kqnrmlem2  24093  reghmph  24142  nrmhmph  24143  filuni  24234  rnelfmlem  24301  fmufil  24308  fclscf  24374  fclsfnflim  24376  flimfnfcls  24377  uffclsflim  24380  cnpfcfi  24389  cnpfcf  24390  alexsublem  24393  alexsubALTlem3  24398  tgpconncompeqg  24461  ghmcnp  24464  qustgplem  24470  blssps  24773  blss  24774  blcld  24854  metequiv2  24859  met2ndci  24871  prdsxmslem2  24878  txmetcnp  24896  nlmvscnlem1  25035  xrge0tsms  25184  ipcnlem1  25596  iscmet3  25644  metsscmetcld  25666  minveclem3  25780  pmltpc  25801  ovolscalem2  25865  ovolicc2lem5  25872  ovolicc2  25873  nulmbl2  25887  ioombl1  25913  uniioombllem6  25939  uniioombl  25940  vitalilem3  25961  i1faddlem  26044  mbfmullem  26076  itg2const2  26092  itg2split  26100  lhop2  26365  dvfsumrlim  26381  itgsubst  26399  plydivex  26648  plyexmo  26666  ulmbdd  26755  cxploglim  27335  dchrptlem2  27622  lgsquad2lem2  27742  2sqlem5  27779  dchrvmasumif  27860  rpvmasum2  27869  dchrisum0re  27870  dchrisum0lem3  27876  dchrisum0  27877  dchrmusum  27881  dchrvmasum  27882  pntibndlem3  27949  pntlemp  27967  ostth3  27995  nna4b4nsq  28020  nosupbday  28092  nosupbnd1lem1  28095  nosupbnd2  28103  noinfbday  28107  noinfbnd1lem1  28110  noinfbnd2  28118  conway  28195  madebdaylemlrcut  28315  mulsproplem9  28540  mulsuniflem  28565  uzsind  28821  bdayfinbndlem1  28883  readdscl  28915  legtrid  29084  hlcgreu  29114  mirreu3  29156  opphllem  29241  oppperpex  29259  lnperpex  29339  trgcopy  29341  iscgra1  29347  cgraswap  29357  cgracom  29359  cgratr  29360  flatcgra  29362  acopyeu  29372  ax5seglem9  29545  ax5seg  29546  axcontlem8  29579  axcontlem12  29583  upgrclwlkcompim  30398  wwlksnextwrd  30516  2pthfrgr  30915  frgrnbnb  30924  ablo4  31182  smcnlem  31329  pjhthmo  31934  tgextahp  33103  1stpreimas  33370  xrge0tsmsd  33704  locfinref  34543  xpinpreima2  34609  qqhval2  34684  dya2iocnrect  34983  orvcgteel  35170  orvclteel  35175  cnpconn  36162  txpconn  36164  connpconn  36167  pconnpi1  36169  iccllysconn  36182  rellysconn  36183  cvmcov2  36207  cvmliftmolem2  36214  cvmliftmo  36216  cvmliftlem15  36230  cvmliftpht  36250  cvmlift3lem2  36252  cgrextend  36951  btwnouttr2  36965  btwnexch2  36966  cgrxfr  36998  lineext  37019  btwnconn1lem5  37034  btwnconn1lem13  37042  btwnconn3  37046  segletr  37057  segleantisym  37058  outsideofeq  37073  outsidele  37075  lineunray  37090  refssfne  37324  neibastop2lem  37326  neibastop2  37327  weiunpo  37431  unblimceq0lem  37550  knoppndvlem22  37577  mblfinlem3  38769  mblfinlem4  38770  cnambfre  38778  itg2addnclem  38781  areacirclem5  38822  istotbnd3  38897  crngm4  39129  cvlcvr1  40588  4atlem12  40861  cdlemb  41043  paddasslem10  41078  paddasslem12  41080  paddasslem13  41081  lhpexle3lem  41260  cdlemd4  41450  cdlemefs32sn1aw  41663  cdleme43fsv1snlem  41669  cdleme32d  41693  cdleme32f  41695  cdleme40m  41716  cdleme40n  41717  cdleme50trn2  41800  cdlemftr3  41814  cdlemm10N  42367  dihvalcqpre  42484  dihopelvalcpre  42497  dihmeetlem1N  42539  dihglblem5apreN  42540  dihmeetlem4preN  42555  dihjat1lem  42677  mapd0  42914  mapdh9a  43038  mzpmfp  43951  mzpcompact2lem  43955  diophin  43976  pellexlem3  44031  pellex  44035  pell14qrmulcl  44063  jm2.19lem3  44191  jm2.25  44199  jm2.27b  44206  hbtlem2  44318  hbtlem5  44322  gsumws3  45388  gsumws4  45389  mnuprdlem1  45448  mnuprdlem2  45449  mnuprdlem4  45451  fnchoice  46251  stoweidlem53  47268  stoweidlem61  47276  qndenserrnbllem  47509  bgoldbtbnd  49112  cycldlenngric  49231  grtrimap  49251  isubgr3stgrlem6  49274  prsthinc  50804  parmapcl2  50975