Theorem simprrr 789

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  prproe  4853  f1prex  7253  fliftfun  7281  fprresex  8275  nnaordex2  8593  naddssim  8640  mapdom2  9105  domunfican  9251  fofinf1o  9261  finsschain  9288  wemaplem3  9482  oemapvali  9625  iunfictbso  10056  enfin2i  10264  fin1a2s  10357  distrlem4pr  10970  mulcmpblnr  11015  prsrlem1  11016  addsrmo  11017  mulsrmo  11018  divdivdiv  11878  divsubdiv  11893  lediv12a  12071  xralrple  13194  seqcaopr  14038  leexp2r  14173  hashbclem  14451  wrd2ind  14722  cshwidxmod  14802  rtrclreclem4  15060  relexpindlem  15062  rtrclind  15064  rlimresb  15564  summo  15716  fsum2dlem  15769  prodmo  15938  fprod2dlem  15982  bezoutlem3  16547  bezoutlem4  16548  qredeu  16664  coprmproddvdslem  16668  prmdvdsncoprmbd  16734  pcqmul  16861  pcadd  16897  pockthg  16914  ramub1lem2  17035  cshwsdisj  17106  mreexexlem4d  17651  issubc3  17854  cofucl  17893  setcmon  18092  setcepi  18093  drsdirfi  18309  poslubmo  18413  posglbmo  18414  grprida  18681  ghmpreima  19250  gaorber  19320  psgnunilem4  19509  psgneu  19518  odcau  19616  pgpssslw  19626  fislw  19637  lsmsubm  19665  efgsfo  19751  pgpfac1  20094  pgpfaclem2  20096  pgpfaclem3  20097  unitgrp  20400  islmodd  20902  lmodprop2d  20960  lsspropd  21053  lbsextlem4  21200  assapropd  21892  evlslem1  22104  mdetunilem8  22648  mdetmul  22652  ppttop  23036  epttop  23038  restbas  23187  iscnp4  23292  cnpco  23296  nrmsep  23386  regsep2  23405  ordthauslem  23412  1stcfb  23474  2ndcctbss  23484  2ndcdisj  23485  2ndcomap  23487  dis2ndc  23489  1stcelcls  23490  nlly2i  23505  islly2  23513  hausllycmp  23523  lly1stc  23525  comppfsc  23561  1stckgenlem  23582  ptbasin  23606  txcls  23633  ptcnp  23651  txlly  23665  txnlly  23666  txtube  23669  txcmplem1  23670  txcmplem2  23671  xkococnlem  23688  basqtop  23740  regr1lem  23768  kqreglem1  23770  kqreglem2  23771  kqnrmlem1  23772  kqnrmlem2  23773  reghmph  23822  nrmhmph  23823  filuni  23914  rnelfmlem  23981  fmufil  23988  fclscf  24054  fclsfnflim  24056  flimfnfcls  24057  uffclsflim  24060  cnpfcfi  24069  cnpfcf  24070  alexsublem  24073  alexsubALTlem3  24078  tgpconncompeqg  24141  ghmcnp  24144  qustgplem  24150  blssps  24453  blss  24454  blcld  24534  metequiv2  24539  met2ndci  24551  prdsxmslem2  24558  txmetcnp  24576  nlmvscnlem1  24715  xrge0tsms  24864  ipcnlem1  25276  iscmet3  25324  metsscmetcld  25346  minveclem3  25460  pmltpc  25481  ovolscalem2  25545  ovolicc2lem5  25552  ovolicc2  25553  nulmbl2  25567  ioombl1  25593  uniioombllem6  25619  uniioombl  25620  vitalilem3  25641  i1faddlem  25724  mbfmullem  25756  itg2const2  25772  itg2split  25780  lhop2  26046  dvfsumrlim  26062  itgsubst  26080  plydivex  26327  plyexmo  26343  ulmbdd  26427  cxploglim  27008  dchrptlem2  27295  lgsquad2lem2  27415  2sqlem5  27452  dchrvmasumif  27533  rpvmasum2  27542  dchrisum0re  27543  dchrisum0lem3  27549  dchrisum0  27550  dchrmusum  27554  dchrvmasum  27555  pntibndlem3  27622  pntlemp  27640  ostth3  27668  nosupbday  27735  nosupbnd1lem1  27738  nosupbnd2  27746  noinfbday  27750  noinfbnd1lem1  27753  noinfbnd2  27761  conway  27838  madebdaylemlrcut  27958  mulsproplem9  28183  mulsuniflem  28208  uzsind  28464  bdayfinbndlem1  28526  readdscl  28558  legtrid  28726  hlcgreu  28753  mirreu3  28789  opphllem  28870  oppperpex  28888  lnperpex  28938  trgcopy  28939  iscgra1  28945  cgraswap  28955  cgracom  28957  cgratr  28958  flatcgra  28959  acopyeu  28969  ax5seglem9  29073  ax5seg  29074  axcontlem8  29107  axcontlem12  29111  upgrclwlkcompim  29916  wwlksnextwrd  30032  2pthfrgr  30421  frgrnbnb  30430  ablo4  30688  smcnlem  30835  pjhthmo  31440  1stpreimas  32847  xrge0tsmsd  33203  locfinref  34082  xpinpreima2  34148  qqhval2  34223  dya2iocnrect  34522  orvcgteel  34709  orvclteel  34714  cnpconn  35518  txpconn  35520  connpconn  35523  pconnpi1  35525  iccllysconn  35538  rellysconn  35539  cvmcov2  35563  cvmliftmolem2  35570  cvmliftmo  35572  cvmliftlem15  35586  cvmliftpht  35606  cvmlift3lem2  35608  cgrextend  36296  btwnouttr2  36310  btwnexch2  36311  cgrxfr  36343  lineext  36364  btwnconn1lem5  36379  btwnconn1lem13  36387  btwnconn3  36391  segletr  36402  segleantisym  36403  outsideofeq  36418  outsidele  36420  lineunray  36435  refssfne  36656  neibastop2lem  36658  neibastop2  36659  weiunpo  36763  unblimceq0lem  36882  knoppndvlem22  36909  mblfinlem3  38096  mblfinlem4  38097  cnambfre  38105  itg2addnclem  38108  areacirclem5  38149  istotbnd3  38208  crngm4  38440  cvlcvr1  39901  4atlem12  40174  cdlemb  40356  paddasslem10  40391  paddasslem12  40393  paddasslem13  40394  lhpexle3lem  40573  cdlemd4  40763  cdlemefs32sn1aw  40976  cdleme43fsv1snlem  40982  cdleme32d  41006  cdleme32f  41008  cdleme40m  41029  cdleme40n  41030  cdleme50trn2  41113  cdlemftr3  41127  cdlemm10N  41680  dihvalcqpre  41797  dihopelvalcpre  41810  dihmeetlem1N  41852  dihglblem5apreN  41853  dihmeetlem4preN  41868  dihjat1lem  41990  mapd0  42227  mapdh9a  42351  nna4b4nsq  43180  mzpmfp  43266  mzpcompact2lem  43270  diophin  43291  pellexlem3  43346  pellex  43350  pell14qrmulcl  43378  jm2.19lem3  43506  jm2.25  43514  jm2.27b  43521  fnwe2lem2  43566  hbtlem2  43639  hbtlem5  43643  gsumws3  44710  gsumws4  44711  mnuprdlem1  44786  mnuprdlem2  44787  mnuprdlem4  44789  fnchoice  45547  stoweidlem53  46565  stoweidlem61  46573  qndenserrnbllem  46806  bgoldbtbnd  48369  cycldlenngric  48488  grtrimap  48508  isubgr3stgrlem6  48531  prsthinc  50023