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  7280  fliftfun  7308  fprresex  8306  nnaordex2  8626  naddssim  8673  mapdom2  9145  domunfican  9291  fofinf1o  9299  finsschain  9326  wemaplem3  9520  oemapvali  9663  iunfictbso  10164  enfin2i  10370  fin1a2s  10463  distrlem4pr  11082  mulcmpblnr  11127  prsrlem1  11128  addsrmo  11129  mulsrmo  11130  divdivdiv  11987  divsubdiv  12002  lediv12a  12179  xralrple  13304  seqcaopr  14150  leexp2r  14285  hashbclem  14564  wrd2ind  14839  cshwidxmod  14921  rtrclreclem4  15181  relexpindlem  15183  rtrclind  15185  rlimresb  15699  summo  15850  fsum2dlem  15903  prodmo  16070  fprod2dlem  16114  bezoutlem3  16678  bezoutlem4  16679  qredeu  16795  coprmproddvdslem  16799  prmdvdsncoprmbd  16865  pcqmul  16992  pcadd  17028  pockthg  17045  ramub1lem2  17166  cshwsdisj  17237  mreexexlem4d  17782  issubc3  17985  cofucl  18024  setcmon  18223  setcepi  18224  drsdirfi  18440  poslubmo  18544  posglbmo  18545  mgmn0plusgf  18788  grprida  18817  ghmpreima  19413  gaorber  19483  psgnunilem4  19672  psgneu  19681  odcau  19779  pgpssslw  19789  fislw  19800  lsmsubm  19828  efgsfo  19914  pgpfac1  20257  pgpfaclem2  20259  pgpfaclem3  20260  unitgrp  20574  islmodd  21102  lmodprop2d  21160  lsspropd  21253  lbsextlem4  21400  assapropd  22140  evlslem1  22352  mdetunilem8  22895  mdetmul  22899  ppttop  23286  epttop  23288  restbas  23437  iscnp4  23542  cnpco  23546  nrmsep  23636  regsep2  23655  ordthauslem  23662  1stcfb  23724  2ndcctbss  23735  2ndcdisj  23736  2ndcomap  23738  dis2ndc  23740  1stcelcls  23741  nlly2i  23756  islly2  23764  hausllycmp  23774  lly1stc  23776  comppfsc  23812  1stckgenlem  23833  ptbasin  23857  txcls  23884  ptcnp  23902  txlly  23916  txnlly  23917  txtube  23920  txcmplem1  23921  txcmplem2  23922  xkococnlem  23939  basqtop  23991  regr1lem  24019  kqreglem1  24021  kqreglem2  24022  kqnrmlem1  24023  kqnrmlem2  24024  reghmph  24073  nrmhmph  24074  filuni  24165  rnelfmlem  24232  fmufil  24239  fclscf  24305  fclsfnflim  24307  flimfnfcls  24308  uffclsflim  24311  cnpfcfi  24320  cnpfcf  24321  alexsublem  24324  alexsubALTlem3  24329  tgpconncompeqg  24392  ghmcnp  24395  qustgplem  24401  blssps  24704  blss  24705  blcld  24785  metequiv2  24790  met2ndci  24802  prdsxmslem2  24809  txmetcnp  24827  nlmvscnlem1  24966  xrge0tsms  25115  ipcnlem1  25527  iscmet3  25575  metsscmetcld  25597  minveclem3  25711  pmltpc  25732  ovolscalem2  25796  ovolicc2lem5  25803  ovolicc2  25804  nulmbl2  25818  ioombl1  25844  uniioombllem6  25870  uniioombl  25871  vitalilem3  25892  i1faddlem  25975  mbfmullem  26007  itg2const2  26023  itg2split  26031  lhop2  26296  dvfsumrlim  26312  itgsubst  26330  plydivex  26581  plyexmo  26599  ulmbdd  26688  cxploglim  27268  dchrptlem2  27555  lgsquad2lem2  27675  2sqlem5  27712  dchrvmasumif  27793  rpvmasum2  27802  dchrisum0re  27803  dchrisum0lem3  27809  dchrisum0  27810  dchrmusum  27814  dchrvmasum  27815  pntibndlem3  27882  pntlemp  27900  ostth3  27928  nosupbday  27995  nosupbnd1lem1  27998  nosupbnd2  28006  noinfbday  28010  noinfbnd1lem1  28013  noinfbnd2  28021  conway  28098  madebdaylemlrcut  28218  mulsproplem9  28443  mulsuniflem  28468  uzsind  28724  bdayfinbndlem1  28786  readdscl  28818  legtrid  28987  hlcgreu  29017  mirreu3  29059  opphllem  29144  oppperpex  29162  lnperpex  29242  trgcopy  29244  iscgra1  29250  cgraswap  29260  cgracom  29262  cgratr  29263  flatcgra  29265  acopyeu  29275  ax5seglem9  29448  ax5seg  29449  axcontlem8  29482  axcontlem12  29486  upgrclwlkcompim  30301  wwlksnextwrd  30419  2pthfrgr  30818  frgrnbnb  30827  ablo4  31085  smcnlem  31232  pjhthmo  31837  1stpreimas  33232  xrge0tsmsd  33567  locfinref  34406  xpinpreima2  34472  qqhval2  34547  dya2iocnrect  34847  orvcgteel  35034  orvclteel  35039  cnpconn  35916  txpconn  35918  connpconn  35921  pconnpi1  35923  iccllysconn  35936  rellysconn  35937  cvmcov2  35961  cvmliftmolem2  35968  cvmliftmo  35970  cvmliftlem15  35984  cvmliftpht  36004  cvmlift3lem2  36006  cgrextend  36695  btwnouttr2  36709  btwnexch2  36710  cgrxfr  36742  lineext  36763  btwnconn1lem5  36778  btwnconn1lem13  36786  btwnconn3  36790  segletr  36801  segleantisym  36802  outsideofeq  36817  outsidele  36819  lineunray  36834  refssfne  37068  neibastop2lem  37070  neibastop2  37071  weiunpo  37175  unblimceq0lem  37294  knoppndvlem22  37321  mblfinlem3  38497  mblfinlem4  38498  cnambfre  38506  itg2addnclem  38509  areacirclem5  38550  istotbnd3  38625  crngm4  38857  cvlcvr1  40316  4atlem12  40589  cdlemb  40771  paddasslem10  40806  paddasslem12  40808  paddasslem13  40809  lhpexle3lem  40988  cdlemd4  41178  cdlemefs32sn1aw  41391  cdleme43fsv1snlem  41397  cdleme32d  41421  cdleme32f  41423  cdleme40m  41444  cdleme40n  41445  cdleme50trn2  41528  cdlemftr3  41542  cdlemm10N  42095  dihvalcqpre  42212  dihopelvalcpre  42225  dihmeetlem1N  42267  dihglblem5apreN  42268  dihmeetlem4preN  42283  dihjat1lem  42405  mapd0  42642  mapdh9a  42766  nna4b4nsq  43610  mzpmfp  43696  mzpcompact2lem  43700  diophin  43721  pellexlem3  43776  pellex  43780  pell14qrmulcl  43808  jm2.19lem3  43936  jm2.25  43944  jm2.27b  43951  fnwe2lem2  43996  hbtlem2  44069  hbtlem5  44073  gsumws3  45140  gsumws4  45141  mnuprdlem1  45200  mnuprdlem2  45201  mnuprdlem4  45203  fnchoice  45967  stoweidlem53  46985  stoweidlem61  46993  qndenserrnbllem  47226  bgoldbtbnd  48829  cycldlenngric  48948  grtrimap  48968  isubgr3stgrlem6  48991  prsthinc  50494