Theorem simprrr 781

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  prproe  4859  f1prex  7225  fliftfun  7253  fprresex  8250  nnaordex2  8564  naddssim  8610  mapdom2  9072  domunfican  9230  fofinf1o  9241  finsschain  9268  wemaplem3  9459  oemapvali  9599  iunfictbso  10027  enfin2i  10234  fin1a2s  10327  distrlem4pr  10939  mulcmpblnr  10984  prsrlem1  10985  addsrmo  10986  mulsrmo  10987  divdivdiv  11843  divsubdiv  11858  lediv12a  12036  xralrple  13125  seqcaopr  13964  leexp2r  14099  hashbclem  14377  wrd2ind  14647  cshwidxmod  14727  rtrclreclem4  14986  relexpindlem  14988  rtrclind  14990  rlimresb  15490  summo  15642  fsum2dlem  15695  prodmo  15861  fprod2dlem  15905  bezoutlem3  16470  bezoutlem4  16471  qredeu  16587  coprmproddvdslem  16591  prmdvdsncoprmbd  16656  pcqmul  16783  pcadd  16819  pockthg  16836  ramub1lem2  16957  cshwsdisj  17028  mreexexlem4d  17571  issubc3  17774  cofucl  17813  setcmon  18012  setcepi  18013  drsdirfi  18229  poslubmo  18333  posglbmo  18334  grprida  18567  ghmpreima  19135  gaorber  19205  psgnunilem4  19394  psgneu  19403  odcau  19501  pgpssslw  19511  fislw  19522  lsmsubm  19550  efgsfo  19636  pgpfac1  19979  pgpfaclem2  19981  pgpfaclem3  19982  unitgrp  20286  islmodd  20787  lmodprop2d  20845  lsspropd  20939  lbsextlem4  21086  assapropd  21797  evlslem1  22005  mdetunilem8  22522  mdetmul  22526  ppttop  22910  epttop  22912  restbas  23061  iscnp4  23166  cnpco  23170  nrmsep  23260  regsep2  23279  ordthauslem  23286  1stcfb  23348  2ndcctbss  23358  2ndcdisj  23359  2ndcomap  23361  dis2ndc  23363  1stcelcls  23364  nlly2i  23379  islly2  23387  hausllycmp  23397  lly1stc  23399  comppfsc  23435  1stckgenlem  23456  ptbasin  23480  txcls  23507  ptcnp  23525  txlly  23539  txnlly  23540  txtube  23543  txcmplem1  23544  txcmplem2  23545  xkococnlem  23562  basqtop  23614  regr1lem  23642  kqreglem1  23644  kqreglem2  23645  kqnrmlem1  23646  kqnrmlem2  23647  reghmph  23696  nrmhmph  23697  filuni  23788  rnelfmlem  23855  fmufil  23862  fclscf  23928  fclsfnflim  23930  flimfnfcls  23931  uffclsflim  23934  cnpfcfi  23943  cnpfcf  23944  alexsublem  23947  alexsubALTlem3  23952  tgpconncompeqg  24015  ghmcnp  24018  qustgplem  24024  blssps  24328  blss  24329  blcld  24409  metequiv2  24414  met2ndci  24426  prdsxmslem2  24433  txmetcnp  24451  nlmvscnlem1  24590  xrge0tsms  24739  ipcnlem1  25161  iscmet3  25209  metsscmetcld  25231  minveclem3  25345  pmltpc  25367  ovolscalem2  25431  ovolicc2lem5  25438  ovolicc2  25439  nulmbl2  25453  ioombl1  25479  uniioombllem6  25505  uniioombl  25506  vitalilem3  25527  i1faddlem  25610  mbfmullem  25642  itg2const2  25658  itg2split  25666  lhop2  25936  dvfsumrlim  25954  itgsubst  25972  plydivex  26221  plyexmo  26237  ulmbdd  26323  cxploglim  26904  dchrptlem2  27192  lgsquad2lem2  27312  2sqlem5  27349  dchrvmasumif  27430  rpvmasum2  27439  dchrisum0re  27440  dchrisum0lem3  27446  dchrisum0  27447  dchrmusum  27451  dchrvmasum  27452  pntibndlem3  27519  pntlemp  27537  ostth3  27565  nosupbday  27633  nosupbnd1lem1  27636  nosupbnd2  27644  noinfbday  27648  noinfbnd1lem1  27651  noinfbnd2  27659  conway  27728  madebdaylemlrcut  27831  mulsproplem9  28050  mulsuniflem  28075  uzsind  28316  readdscl  28386  legtrid  28554  hlcgreu  28581  mirreu3  28617  opphllem  28698  oppperpex  28716  lnperpex  28766  trgcopy  28767  iscgra1  28773  cgraswap  28783  cgracom  28785  cgratr  28786  flatcgra  28787  acopyeu  28797  ax5seglem9  28900  ax5seg  28901  axcontlem8  28934  axcontlem12  28938  upgrclwlkcompim  29744  wwlksnextwrd  29860  2pthfrgr  30246  frgrnbnb  30255  ablo4  30512  smcnlem  30659  pjhthmo  31264  1stpreimas  32662  xrge0tsmsd  33028  locfinref  33807  xpinpreima2  33873  qqhval2  33948  dya2iocnrect  34248  orvcgteel  34435  orvclteel  34440  cnpconn  35202  txpconn  35204  connpconn  35207  pconnpi1  35209  iccllysconn  35222  rellysconn  35223  cvmcov2  35247  cvmliftmolem2  35254  cvmliftmo  35256  cvmliftlem15  35270  cvmliftpht  35290  cvmlift3lem2  35292  cgrextend  35981  btwnouttr2  35995  btwnexch2  35996  cgrxfr  36028  lineext  36049  btwnconn1lem5  36064  btwnconn1lem13  36072  btwnconn3  36076  segletr  36087  segleantisym  36088  outsideofeq  36103  outsidele  36105  lineunray  36120  refssfne  36331  neibastop2lem  36333  neibastop2  36334  weiunpo  36438  unblimceq0lem  36479  knoppndvlem22  36506  mblfinlem3  37638  mblfinlem4  37639  cnambfre  37647  itg2addnclem  37650  areacirclem5  37691  istotbnd3  37750  crngm4  37982  cvlcvr1  39317  4atlem12  39591  cdlemb  39773  paddasslem10  39808  paddasslem12  39810  paddasslem13  39811  lhpexle3lem  39990  cdlemd4  40180  cdlemefs32sn1aw  40393  cdleme43fsv1snlem  40399  cdleme32d  40423  cdleme32f  40425  cdleme40m  40446  cdleme40n  40447  cdleme50trn2  40530  cdlemftr3  40544  cdlemm10N  41097  dihvalcqpre  41214  dihopelvalcpre  41227  dihmeetlem1N  41269  dihglblem5apreN  41270  dihmeetlem4preN  41285  dihjat1lem  41407  mapd0  41644  mapdh9a  41768  nna4b4nsq  42633  mzpmfp  42720  mzpcompact2lem  42724  diophin  42745  pellexlem3  42804  pellex  42808  pell14qrmulcl  42836  jm2.19lem3  42964  jm2.25  42972  jm2.27b  42979  fnwe2lem2  43024  hbtlem2  43097  hbtlem5  43101  gsumws3  44169  gsumws4  44170  mnuprdlem1  44245  mnuprdlem2  44246  mnuprdlem4  44248  fnchoice  45007  stoweidlem53  46035  stoweidlem61  46043  qndenserrnbllem  46276  bgoldbtbnd  47794  cycldlenngric  47912  grtrimap  47931  isubgr3stgrlem6  47954  prsthinc  49437