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  4856  f1prex  7224  fliftfun  7252  fprresex  8246  nnaordex2  8560  naddssim  8606  mapdom2  9067  domunfican  9212  fofinf1o  9222  finsschain  9249  wemaplem3  9440  oemapvali  9580  iunfictbso  10011  enfin2i  10218  fin1a2s  10311  distrlem4pr  10923  mulcmpblnr  10968  prsrlem1  10969  addsrmo  10970  mulsrmo  10971  divdivdiv  11828  divsubdiv  11843  lediv12a  12021  xralrple  13110  seqcaopr  13952  leexp2r  14087  hashbclem  14365  wrd2ind  14636  cshwidxmod  14716  rtrclreclem4  14974  relexpindlem  14976  rtrclind  14978  rlimresb  15478  summo  15630  fsum2dlem  15683  prodmo  15849  fprod2dlem  15893  bezoutlem3  16458  bezoutlem4  16459  qredeu  16575  coprmproddvdslem  16579  prmdvdsncoprmbd  16644  pcqmul  16771  pcadd  16807  pockthg  16824  ramub1lem2  16945  cshwsdisj  17016  mreexexlem4d  17559  issubc3  17762  cofucl  17801  setcmon  18000  setcepi  18001  drsdirfi  18217  poslubmo  18321  posglbmo  18322  grprida  18589  ghmpreima  19156  gaorber  19226  psgnunilem4  19415  psgneu  19424  odcau  19522  pgpssslw  19532  fislw  19543  lsmsubm  19571  efgsfo  19657  pgpfac1  20000  pgpfaclem2  20002  pgpfaclem3  20003  unitgrp  20307  islmodd  20805  lmodprop2d  20863  lsspropd  20957  lbsextlem4  21104  assapropd  21815  evlslem1  22023  mdetunilem8  22540  mdetmul  22544  ppttop  22928  epttop  22930  restbas  23079  iscnp4  23184  cnpco  23188  nrmsep  23278  regsep2  23297  ordthauslem  23304  1stcfb  23366  2ndcctbss  23376  2ndcdisj  23377  2ndcomap  23379  dis2ndc  23381  1stcelcls  23382  nlly2i  23397  islly2  23405  hausllycmp  23415  lly1stc  23417  comppfsc  23453  1stckgenlem  23474  ptbasin  23498  txcls  23525  ptcnp  23543  txlly  23557  txnlly  23558  txtube  23561  txcmplem1  23562  txcmplem2  23563  xkococnlem  23580  basqtop  23632  regr1lem  23660  kqreglem1  23662  kqreglem2  23663  kqnrmlem1  23664  kqnrmlem2  23665  reghmph  23714  nrmhmph  23715  filuni  23806  rnelfmlem  23873  fmufil  23880  fclscf  23946  fclsfnflim  23948  flimfnfcls  23949  uffclsflim  23952  cnpfcfi  23961  cnpfcf  23962  alexsublem  23965  alexsubALTlem3  23970  tgpconncompeqg  24033  ghmcnp  24036  qustgplem  24042  blssps  24345  blss  24346  blcld  24426  metequiv2  24431  met2ndci  24443  prdsxmslem2  24450  txmetcnp  24468  nlmvscnlem1  24607  xrge0tsms  24756  ipcnlem1  25178  iscmet3  25226  metsscmetcld  25248  minveclem3  25362  pmltpc  25384  ovolscalem2  25448  ovolicc2lem5  25455  ovolicc2  25456  nulmbl2  25470  ioombl1  25496  uniioombllem6  25522  uniioombl  25523  vitalilem3  25544  i1faddlem  25627  mbfmullem  25659  itg2const2  25675  itg2split  25683  lhop2  25953  dvfsumrlim  25971  itgsubst  25989  plydivex  26238  plyexmo  26254  ulmbdd  26340  cxploglim  26921  dchrptlem2  27209  lgsquad2lem2  27329  2sqlem5  27366  dchrvmasumif  27447  rpvmasum2  27456  dchrisum0re  27457  dchrisum0lem3  27463  dchrisum0  27464  dchrmusum  27468  dchrvmasum  27469  pntibndlem3  27536  pntlemp  27554  ostth3  27582  nosupbday  27650  nosupbnd1lem1  27653  nosupbnd2  27661  noinfbday  27665  noinfbnd1lem1  27668  noinfbnd2  27676  conway  27746  madebdaylemlrcut  27850  mulsproplem9  28069  mulsuniflem  28094  uzsind  28335  readdscl  28407  legtrid  28575  hlcgreu  28602  mirreu3  28638  opphllem  28719  oppperpex  28737  lnperpex  28787  trgcopy  28788  iscgra1  28794  cgraswap  28804  cgracom  28806  cgratr  28807  flatcgra  28808  acopyeu  28818  ax5seglem9  28922  ax5seg  28923  axcontlem8  28956  axcontlem12  28960  upgrclwlkcompim  29766  wwlksnextwrd  29882  2pthfrgr  30271  frgrnbnb  30280  ablo4  30537  smcnlem  30684  pjhthmo  31289  1stpreimas  32694  xrge0tsmsd  33049  locfinref  33861  xpinpreima2  33927  qqhval2  34002  dya2iocnrect  34301  orvcgteel  34488  orvclteel  34493  cnpconn  35281  txpconn  35283  connpconn  35286  pconnpi1  35288  iccllysconn  35301  rellysconn  35302  cvmcov2  35326  cvmliftmolem2  35333  cvmliftmo  35335  cvmliftlem15  35349  cvmliftpht  35369  cvmlift3lem2  35371  cgrextend  36059  btwnouttr2  36073  btwnexch2  36074  cgrxfr  36106  lineext  36127  btwnconn1lem5  36142  btwnconn1lem13  36150  btwnconn3  36154  segletr  36165  segleantisym  36166  outsideofeq  36181  outsidele  36183  lineunray  36198  refssfne  36409  neibastop2lem  36411  neibastop2  36412  weiunpo  36516  unblimceq0lem  36557  knoppndvlem22  36584  mblfinlem3  37705  mblfinlem4  37706  cnambfre  37714  itg2addnclem  37717  areacirclem5  37758  istotbnd3  37817  crngm4  38049  cvlcvr1  39444  4atlem12  39717  cdlemb  39899  paddasslem10  39934  paddasslem12  39936  paddasslem13  39937  lhpexle3lem  40116  cdlemd4  40306  cdlemefs32sn1aw  40519  cdleme43fsv1snlem  40525  cdleme32d  40549  cdleme32f  40551  cdleme40m  40572  cdleme40n  40573  cdleme50trn2  40656  cdlemftr3  40670  cdlemm10N  41223  dihvalcqpre  41340  dihopelvalcpre  41353  dihmeetlem1N  41395  dihglblem5apreN  41396  dihmeetlem4preN  41411  dihjat1lem  41533  mapd0  41770  mapdh9a  41894  nna4b4nsq  42759  mzpmfp  42845  mzpcompact2lem  42849  diophin  42870  pellexlem3  42929  pellex  42933  pell14qrmulcl  42961  jm2.19lem3  43089  jm2.25  43097  jm2.27b  43104  fnwe2lem2  43149  hbtlem2  43222  hbtlem5  43226  gsumws3  44294  gsumws4  44295  mnuprdlem1  44370  mnuprdlem2  44371  mnuprdlem4  44373  fnchoice  45131  stoweidlem53  46156  stoweidlem61  46164  qndenserrnbllem  46397  bgoldbtbnd  47914  cycldlenngric  48033  grtrimap  48053  isubgr3stgrlem6  48076  prsthinc  49570