Theorem simprrr 780

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 727	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  4838  f1prex  7042  fliftfun  7067  wfrlem17  7973  mapdom2  8690  domunfican  8793  fofinf1o  8801  finsschain  8833  wemaplem3  9014  oemapvali  9149  iunfictbso  9542  enfin2i  9745  fin1a2s  9838  distrlem4pr  10450  mulcmpblnr  10495  prsrlem1  10496  addsrmo  10497  mulsrmo  10498  divdivdiv  11343  divsubdiv  11358  lediv12a  11535  xralrple  12601  seqcaopr  13410  leexp2r  13541  hashbclem  13813  wrd2ind  14087  cshwidxmod  14167  rtrclreclem4  14422  relexpindlem  14424  rtrclind  14426  rlimresb  14924  summo  15076  fsum2dlem  15127  prodmo  15292  fprod2dlem  15336  bezoutlem3  15891  bezoutlem4  15892  qredeu  16004  coprmproddvdslem  16008  pcqmul  16192  pcadd  16227  pockthg  16244  ramub1lem2  16365  cshwsdisj  16434  mreexexlem4d  16920  issubc3  17121  cofucl  17160  setcmon  17349  setcepi  17350  drsdirfi  17550  poslubmo  17758  posglbmo  17759  grpridd  17887  ghmpreima  18382  gaorber  18440  psgnunilem4  18627  psgneu  18636  odcau  18731  pgpssslw  18741  fislw  18752  lsmsubm  18780  efgsfo  18867  pgpfac1  19204  pgpfaclem2  19206  pgpfaclem3  19207  unitgrp  19419  islmodd  19642  lmodprop2d  19698  lsspropd  19791  lbsextlem4  19935  assapropd  20103  evlslem1  20297  mdetunilem8  21230  mdetmul  21234  ppttop  21617  epttop  21619  restbas  21768  iscnp4  21873  cnpco  21877  nrmsep  21967  regsep2  21986  ordthauslem  21993  1stcfb  22055  2ndcctbss  22065  2ndcdisj  22066  2ndcomap  22068  dis2ndc  22070  1stcelcls  22071  nlly2i  22086  islly2  22094  hausllycmp  22104  lly1stc  22106  comppfsc  22142  1stckgenlem  22163  ptbasin  22187  txcls  22214  ptcnp  22232  txlly  22246  txnlly  22247  txtube  22250  txcmplem1  22251  txcmplem2  22252  xkococnlem  22269  basqtop  22321  regr1lem  22349  kqreglem1  22351  kqreglem2  22352  kqnrmlem1  22353  kqnrmlem2  22354  reghmph  22403  nrmhmph  22404  filuni  22495  rnelfmlem  22562  fmufil  22569  fclscf  22635  fclsfnflim  22637  flimfnfcls  22638  uffclsflim  22641  cnpfcfi  22650  cnpfcf  22651  alexsublem  22654  alexsubALTlem3  22659  tgpconncompeqg  22722  ghmcnp  22725  qustgplem  22731  blssps  23036  blss  23037  blcld  23117  metequiv2  23122  met2ndci  23134  prdsxmslem2  23141  txmetcnp  23159  nlmvscnlem1  23297  xrge0tsms  23444  ipcnlem1  23850  iscmet3  23898  metsscmetcld  23920  minveclem3  24034  pmltpc  24053  ovolscalem2  24117  ovolicc2lem5  24124  ovolicc2  24125  nulmbl2  24139  ioombl1  24165  uniioombllem6  24191  uniioombl  24192  vitalilem3  24213  i1faddlem  24296  mbfmullem  24328  itg2const2  24344  itg2split  24352  lhop2  24614  dvfsumrlim  24630  itgsubst  24648  plydivex  24888  plyexmo  24904  ulmbdd  24988  cxploglim  25557  dchrptlem2  25843  lgsquad2lem2  25963  2sqlem5  26000  dchrvmasumif  26081  rpvmasum2  26090  dchrisum0re  26091  dchrisum0lem3  26097  dchrisum0  26098  dchrmusum  26102  dchrvmasum  26103  pntibndlem3  26170  pntlemp  26188  ostth3  26216  legtrid  26379  hlcgreu  26406  mirreu3  26442  opphllem  26523  oppperpex  26541  lnperpex  26591  trgcopy  26592  iscgra1  26598  cgraswap  26608  cgracom  26610  cgratr  26611  flatcgra  26612  acopyeu  26622  ax5seglem9  26725  ax5seg  26726  axcontlem8  26759  axcontlem12  26763  upgrclwlkcompim  27564  wwlksnextwrd  27677  2pthfrgr  28065  frgrnbnb  28074  ablo4  28329  smcnlem  28476  pjhthmo  29081  1stpreimas  30443  xrge0tsmsd  30694  locfinref  31107  xpinpreima2  31152  qqhval2  31225  dya2iocnrect  31541  orvcgteel  31727  orvclteel  31732  cnpconn  32479  txpconn  32481  connpconn  32484  pconnpi1  32486  iccllysconn  32499  rellysconn  32500  cvmcov2  32524  cvmliftmolem2  32531  cvmliftmo  32533  cvmliftlem15  32547  cvmliftpht  32567  cvmlift3lem2  32569  nosupbnd1lem1  33210  nosupbnd2  33218  conway  33266  cgrextend  33471  btwnouttr2  33485  btwnexch2  33486  cgrxfr  33518  lineext  33539  btwnconn1lem5  33554  btwnconn1lem13  33562  btwnconn3  33566  segletr  33577  segleantisym  33578  outsideofeq  33593  outsidele  33595  lineunray  33610  refssfne  33708  neibastop2lem  33710  neibastop2  33711  unblimceq0lem  33847  knoppndvlem22  33874  mblfinlem3  34933  mblfinlem4  34934  cnambfre  34942  itg2addnclem  34945  areacirclem5  34988  istotbnd3  35051  crngm4  35283  cvlcvr1  36477  4atlem12  36750  cdlemb  36932  paddasslem10  36967  paddasslem12  36969  paddasslem13  36970  lhpexle3lem  37149  cdlemd4  37339  cdlemefs32sn1aw  37552  cdleme43fsv1snlem  37558  cdleme32d  37582  cdleme32f  37584  cdleme40m  37605  cdleme40n  37606  cdleme50trn2  37689  cdlemftr3  37703  cdlemm10N  38256  dihvalcqpre  38373  dihopelvalcpre  38386  dihmeetlem1N  38428  dihglblem5apreN  38429  dihmeetlem4preN  38444  dihjat1lem  38566  mapd0  38803  mapdh9a  38927  mzpmfp  39351  mzpcompact2lem  39355  diophin  39376  pellexlem3  39435  pellex  39439  pell14qrmulcl  39467  jm2.19lem3  39595  jm2.25  39603  jm2.27b  39610  fnwe2lem2  39658  hbtlem2  39731  hbtlem5  39735  gsumws3  40556  gsumws4  40557  mnuprdlem1  40615  mnuprdlem2  40616  mnuprdlem4  40618  fnchoice  41293  stoweidlem53  42345  stoweidlem61  42353  qndenserrnbllem  42586  bgoldbtbnd  43981