Theorem simprrr 782

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 730	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  4849  f1prex  7230  fliftfun  7258  fprresex  8251  nnaordex2  8566  naddssim  8612  mapdom2  9077  domunfican  9223  fofinf1o  9233  finsschain  9260  wemaplem3  9454  oemapvali  9594  iunfictbso  10025  enfin2i  10232  fin1a2s  10325  distrlem4pr  10938  mulcmpblnr  10983  prsrlem1  10984  addsrmo  10985  mulsrmo  10986  divdivdiv  11843  divsubdiv  11858  lediv12a  12036  xralrple  13121  seqcaopr  13963  leexp2r  14098  hashbclem  14376  wrd2ind  14647  cshwidxmod  14727  rtrclreclem4  14985  relexpindlem  14987  rtrclind  14989  rlimresb  15489  summo  15641  fsum2dlem  15694  prodmo  15860  fprod2dlem  15904  bezoutlem3  16469  bezoutlem4  16470  qredeu  16586  coprmproddvdslem  16590  prmdvdsncoprmbd  16655  pcqmul  16782  pcadd  16818  pockthg  16835  ramub1lem2  16956  cshwsdisj  17027  mreexexlem4d  17571  issubc3  17774  cofucl  17813  setcmon  18012  setcepi  18013  drsdirfi  18229  poslubmo  18333  posglbmo  18334  grprida  18601  ghmpreima  19171  gaorber  19241  psgnunilem4  19430  psgneu  19439  odcau  19537  pgpssslw  19547  fislw  19558  lsmsubm  19586  efgsfo  19672  pgpfac1  20015  pgpfaclem2  20017  pgpfaclem3  20018  unitgrp  20321  islmodd  20819  lmodprop2d  20877  lsspropd  20971  lbsextlem4  21118  assapropd  21828  evlslem1  22038  mdetunilem8  22562  mdetmul  22566  ppttop  22950  epttop  22952  restbas  23101  iscnp4  23206  cnpco  23210  nrmsep  23300  regsep2  23319  ordthauslem  23326  1stcfb  23388  2ndcctbss  23398  2ndcdisj  23399  2ndcomap  23401  dis2ndc  23403  1stcelcls  23404  nlly2i  23419  islly2  23427  hausllycmp  23437  lly1stc  23439  comppfsc  23475  1stckgenlem  23496  ptbasin  23520  txcls  23547  ptcnp  23565  txlly  23579  txnlly  23580  txtube  23583  txcmplem1  23584  txcmplem2  23585  xkococnlem  23602  basqtop  23654  regr1lem  23682  kqreglem1  23684  kqreglem2  23685  kqnrmlem1  23686  kqnrmlem2  23687  reghmph  23736  nrmhmph  23737  filuni  23828  rnelfmlem  23895  fmufil  23902  fclscf  23968  fclsfnflim  23970  flimfnfcls  23971  uffclsflim  23974  cnpfcfi  23983  cnpfcf  23984  alexsublem  23987  alexsubALTlem3  23992  tgpconncompeqg  24055  ghmcnp  24058  qustgplem  24064  blssps  24367  blss  24368  blcld  24448  metequiv2  24453  met2ndci  24465  prdsxmslem2  24472  txmetcnp  24490  nlmvscnlem1  24629  xrge0tsms  24778  ipcnlem1  25190  iscmet3  25238  metsscmetcld  25260  minveclem3  25374  pmltpc  25395  ovolscalem2  25459  ovolicc2lem5  25466  ovolicc2  25467  nulmbl2  25481  ioombl1  25507  uniioombllem6  25533  uniioombl  25534  vitalilem3  25555  i1faddlem  25638  mbfmullem  25670  itg2const2  25686  itg2split  25694  lhop2  25961  dvfsumrlim  25979  itgsubst  25997  plydivex  26245  plyexmo  26261  ulmbdd  26347  cxploglim  26928  dchrptlem2  27216  lgsquad2lem2  27336  2sqlem5  27373  dchrvmasumif  27454  rpvmasum2  27463  dchrisum0re  27464  dchrisum0lem3  27470  dchrisum0  27471  dchrmusum  27475  dchrvmasum  27476  pntibndlem3  27543  pntlemp  27561  ostth3  27589  nosupbday  27657  nosupbnd1lem1  27660  nosupbnd2  27668  noinfbday  27672  noinfbnd1lem1  27675  noinfbnd2  27683  conway  27759  madebdaylemlrcut  27879  mulsproplem9  28104  mulsuniflem  28129  uzsind  28385  bdayfinbndlem1  28447  readdscl  28479  legtrid  28647  hlcgreu  28674  mirreu3  28710  opphllem  28791  oppperpex  28809  lnperpex  28859  trgcopy  28860  iscgra1  28866  cgraswap  28876  cgracom  28878  cgratr  28879  flatcgra  28880  acopyeu  28890  ax5seglem9  28994  ax5seg  28995  axcontlem8  29028  axcontlem12  29032  upgrclwlkcompim  29838  wwlksnextwrd  29954  2pthfrgr  30343  frgrnbnb  30352  ablo4  30610  smcnlem  30757  pjhthmo  31362  1stpreimas  32768  xrge0tsmsd  33139  locfinref  33991  xpinpreima2  34057  qqhval2  34132  dya2iocnrect  34431  orvcgteel  34618  orvclteel  34623  cnpconn  35418  txpconn  35420  connpconn  35423  pconnpi1  35425  iccllysconn  35438  rellysconn  35439  cvmcov2  35463  cvmliftmolem2  35470  cvmliftmo  35472  cvmliftlem15  35486  cvmliftpht  35506  cvmlift3lem2  35508  cgrextend  36196  btwnouttr2  36210  btwnexch2  36211  cgrxfr  36243  lineext  36264  btwnconn1lem5  36279  btwnconn1lem13  36287  btwnconn3  36291  segletr  36302  segleantisym  36303  outsideofeq  36318  outsidele  36320  lineunray  36335  refssfne  36546  neibastop2lem  36548  neibastop2  36549  weiunpo  36653  unblimceq0lem  36764  knoppndvlem22  36791  mblfinlem3  37971  mblfinlem4  37972  cnambfre  37980  itg2addnclem  37983  areacirclem5  38024  istotbnd3  38083  crngm4  38315  cvlcvr1  39776  4atlem12  40049  cdlemb  40231  paddasslem10  40266  paddasslem12  40268  paddasslem13  40269  lhpexle3lem  40448  cdlemd4  40638  cdlemefs32sn1aw  40851  cdleme43fsv1snlem  40857  cdleme32d  40881  cdleme32f  40883  cdleme40m  40904  cdleme40n  40905  cdleme50trn2  40988  cdlemftr3  41002  cdlemm10N  41555  dihvalcqpre  41672  dihopelvalcpre  41685  dihmeetlem1N  41727  dihglblem5apreN  41728  dihmeetlem4preN  41743  dihjat1lem  41865  mapd0  42102  mapdh9a  42226  nna4b4nsq  43092  mzpmfp  43178  mzpcompact2lem  43182  diophin  43203  pellexlem3  43262  pellex  43266  pell14qrmulcl  43294  jm2.19lem3  43422  jm2.25  43430  jm2.27b  43437  fnwe2lem2  43482  hbtlem2  43555  hbtlem5  43559  gsumws3  44626  gsumws4  44627  mnuprdlem1  44702  mnuprdlem2  44703  mnuprdlem4  44705  fnchoice  45463  stoweidlem53  46485  stoweidlem61  46493  qndenserrnbllem  46726  bgoldbtbnd  48243  cycldlenngric  48362  grtrimap  48382  isubgr3stgrlem6  48405  prsthinc  49897