Theorem simprrr 793

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

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

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 401

This theorem is used by:  prproe  4869  f1prex  7282  fliftfun  7310  fprresex  8305  nnaordex2  8623  naddssim  8670  mapdom2  9134  domunfican  9279  fofinf1o  9287  finsschain  9314  wemaplem3  9508  oemapvali  9651  iunfictbso  10105  enfin2i  10311  fin1a2s  10404  distrlem4pr  11017  mulcmpblnr  11062  prsrlem1  11063  addsrmo  11064  mulsrmo  11065  divdivdiv  11922  divsubdiv  11937  lediv12a  12114  xralrple  13237  seqcaopr  14082  leexp2r  14217  hashbclem  14496  wrd2ind  14767  cshwidxmod  14847  rtrclreclem4  15105  relexpindlem  15107  rtrclind  15109  rlimresb  15623  summo  15775  fsum2dlem  15828  prodmo  15997  fprod2dlem  16041  bezoutlem3  16605  bezoutlem4  16606  qredeu  16722  coprmproddvdslem  16726  prmdvdsncoprmbd  16792  pcqmul  16919  pcadd  16955  pockthg  16972  ramub1lem2  17093  cshwsdisj  17164  mreexexlem4d  17709  issubc3  17912  cofucl  17951  setcmon  18150  setcepi  18151  drsdirfi  18367  poslubmo  18471  posglbmo  18472  grprida  18739  ghmpreima  19314  gaorber  19384  psgnunilem4  19573  psgneu  19582  odcau  19680  pgpssslw  19690  fislw  19701  lsmsubm  19729  efgsfo  19815  pgpfac1  20158  pgpfaclem2  20160  pgpfaclem3  20161  unitgrp  20472  islmodd  20998  lmodprop2d  21056  lsspropd  21149  lbsextlem4  21296  assapropd  22032  evlslem1  22244  mdetunilem8  22787  mdetmul  22791  ppttop  23175  epttop  23177  restbas  23326  iscnp4  23431  cnpco  23435  nrmsep  23525  regsep2  23544  ordthauslem  23551  1stcfb  23613  2ndcctbss  23623  2ndcdisj  23624  2ndcomap  23626  dis2ndc  23628  1stcelcls  23629  nlly2i  23644  islly2  23652  hausllycmp  23662  lly1stc  23664  comppfsc  23700  1stckgenlem  23721  ptbasin  23745  txcls  23772  ptcnp  23790  txlly  23804  txnlly  23805  txtube  23808  txcmplem1  23809  txcmplem2  23810  xkococnlem  23827  basqtop  23879  regr1lem  23907  kqreglem1  23909  kqreglem2  23910  kqnrmlem1  23911  kqnrmlem2  23912  reghmph  23961  nrmhmph  23962  filuni  24053  rnelfmlem  24120  fmufil  24127  fclscf  24193  fclsfnflim  24195  flimfnfcls  24196  uffclsflim  24199  cnpfcfi  24208  cnpfcf  24209  alexsublem  24212  alexsubALTlem3  24217  tgpconncompeqg  24280  ghmcnp  24283  qustgplem  24289  blssps  24592  blss  24593  blcld  24673  metequiv2  24678  met2ndci  24690  prdsxmslem2  24697  txmetcnp  24715  nlmvscnlem1  24854  xrge0tsms  25003  ipcnlem1  25415  iscmet3  25463  metsscmetcld  25485  minveclem3  25599  pmltpc  25620  ovolscalem2  25684  ovolicc2lem5  25691  ovolicc2  25692  nulmbl2  25706  ioombl1  25732  uniioombllem6  25758  uniioombl  25759  vitalilem3  25780  i1faddlem  25863  mbfmullem  25895  itg2const2  25911  itg2split  25919  lhop2  26185  dvfsumrlim  26201  itgsubst  26219  plydivex  26469  plyexmo  26485  ulmbdd  26572  cxploglim  27153  dchrptlem2  27440  lgsquad2lem2  27560  2sqlem5  27597  dchrvmasumif  27678  rpvmasum2  27687  dchrisum0re  27688  dchrisum0lem3  27694  dchrisum0  27695  dchrmusum  27699  dchrvmasum  27700  pntibndlem3  27767  pntlemp  27785  ostth3  27813  nosupbday  27880  nosupbnd1lem1  27883  nosupbnd2  27891  noinfbday  27895  noinfbnd1lem1  27898  noinfbnd2  27906  conway  27983  madebdaylemlrcut  28103  mulsproplem9  28328  mulsuniflem  28353  uzsind  28609  bdayfinbndlem1  28671  readdscl  28703  legtrid  28871  hlcgreu  28901  mirreu3  28942  opphllem  29027  oppperpex  29045  lnperpex  29124  trgcopy  29126  iscgra1  29132  cgraswap  29142  cgracom  29144  cgratr  29145  flatcgra  29146  acopyeu  29156  ax5seglem9  29298  ax5seg  29299  axcontlem8  29332  axcontlem12  29336  upgrclwlkcompim  30141  wwlksnextwrd  30257  2pthfrgr  30646  frgrnbnb  30655  ablo4  30913  smcnlem  31060  pjhthmo  31665  1stpreimas  33062  xrge0tsmsd  33402  locfinref  34240  xpinpreima2  34306  qqhval2  34381  dya2iocnrect  34680  orvcgteel  34867  orvclteel  34872  cnpconn  35730  txpconn  35732  connpconn  35735  pconnpi1  35737  iccllysconn  35750  rellysconn  35751  cvmcov2  35775  cvmliftmolem2  35782  cvmliftmo  35784  cvmliftlem15  35798  cvmliftpht  35818  cvmlift3lem2  35820  cgrextend  36508  btwnouttr2  36522  btwnexch2  36523  cgrxfr  36555  lineext  36576  btwnconn1lem5  36591  btwnconn1lem13  36599  btwnconn3  36603  segletr  36614  segleantisym  36615  outsideofeq  36630  outsidele  36632  lineunray  36647  refssfne  36897  neibastop2lem  36899  neibastop2  36900  weiunpo  37004  unblimceq0lem  37123  knoppndvlem22  37150  mblfinlem3  38338  mblfinlem4  38339  cnambfre  38347  itg2addnclem  38350  areacirclem5  38391  istotbnd3  38450  crngm4  38682  cvlcvr1  40141  4atlem12  40414  cdlemb  40596  paddasslem10  40631  paddasslem12  40633  paddasslem13  40634  lhpexle3lem  40813  cdlemd4  41003  cdlemefs32sn1aw  41216  cdleme43fsv1snlem  41222  cdleme32d  41246  cdleme32f  41248  cdleme40m  41269  cdleme40n  41270  cdleme50trn2  41353  cdlemftr3  41367  cdlemm10N  41920  dihvalcqpre  42037  dihopelvalcpre  42050  dihmeetlem1N  42092  dihglblem5apreN  42093  dihmeetlem4preN  42108  dihjat1lem  42230  mapd0  42467  mapdh9a  42591  nna4b4nsq  43420  mzpmfp  43506  mzpcompact2lem  43510  diophin  43531  pellexlem3  43586  pellex  43590  pell14qrmulcl  43618  jm2.19lem3  43746  jm2.25  43754  jm2.27b  43761  fnwe2lem2  43806  hbtlem2  43879  hbtlem5  43883  gsumws3  44950  gsumws4  44951  mnuprdlem1  45010  mnuprdlem2  45011  mnuprdlem4  45013  fnchoice  45777  stoweidlem53  46795  stoweidlem61  46803  qndenserrnbllem  47036  bgoldbtbnd  48602  cycldlenngric  48721  grtrimap  48741  isubgr3stgrlem6  48764  prsthinc  50270