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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  prproe  4868  f1prex  7235  fliftfun  7262  fprresex  8246  wfrlem17OLD  8276  naddssim  8636  mapdom2  9099  domunfican  9271  fofinf1o  9278  finsschain  9310  wemaplem3  9493  oemapvali  9629  iunfictbso  10059  enfin2i  10266  fin1a2s  10359  distrlem4pr  10971  mulcmpblnr  11016  prsrlem1  11017  addsrmo  11018  mulsrmo  11019  divdivdiv  11865  divsubdiv  11880  lediv12a  12057  xralrple  13134  seqcaopr  13955  leexp2r  14089  hashbclem  14361  wrd2ind  14623  cshwidxmod  14703  rtrclreclem4  14958  relexpindlem  14960  rtrclind  14962  rlimresb  15459  summo  15613  fsum2dlem  15666  prodmo  15830  fprod2dlem  15874  bezoutlem3  16433  bezoutlem4  16434  qredeu  16545  coprmproddvdslem  16549  prmdvdsncoprmbd  16613  pcqmul  16736  pcadd  16772  pockthg  16789  ramub1lem2  16910  cshwsdisj  16982  mreexexlem4d  17541  issubc3  17749  cofucl  17788  setcmon  17987  setcepi  17988  drsdirfi  18208  poslubmo  18314  posglbmo  18315  grpridd  18544  ghmpreima  19044  gaorber  19102  psgnunilem4  19293  psgneu  19302  odcau  19400  pgpssslw  19410  fislw  19421  lsmsubm  19449  efgsfo  19535  pgpfac1  19873  pgpfaclem2  19875  pgpfaclem3  19876  unitgrp  20110  islmodd  20384  lmodprop2d  20441  lsspropd  20535  lbsextlem4  20681  assapropd  21312  evlslem1  21529  mdetunilem8  22005  mdetmul  22009  ppttop  22394  epttop  22396  restbas  22546  iscnp4  22651  cnpco  22655  nrmsep  22745  regsep2  22764  ordthauslem  22771  1stcfb  22833  2ndcctbss  22843  2ndcdisj  22844  2ndcomap  22846  dis2ndc  22848  1stcelcls  22849  nlly2i  22864  islly2  22872  hausllycmp  22882  lly1stc  22884  comppfsc  22920  1stckgenlem  22941  ptbasin  22965  txcls  22992  ptcnp  23010  txlly  23024  txnlly  23025  txtube  23028  txcmplem1  23029  txcmplem2  23030  xkococnlem  23047  basqtop  23099  regr1lem  23127  kqreglem1  23129  kqreglem2  23130  kqnrmlem1  23131  kqnrmlem2  23132  reghmph  23181  nrmhmph  23182  filuni  23273  rnelfmlem  23340  fmufil  23347  fclscf  23413  fclsfnflim  23415  flimfnfcls  23416  uffclsflim  23419  cnpfcfi  23428  cnpfcf  23429  alexsublem  23432  alexsubALTlem3  23437  tgpconncompeqg  23500  ghmcnp  23503  qustgplem  23509  blssps  23814  blss  23815  blcld  23898  metequiv2  23903  met2ndci  23915  prdsxmslem2  23922  txmetcnp  23940  nlmvscnlem1  24087  xrge0tsms  24234  ipcnlem1  24646  iscmet3  24694  metsscmetcld  24716  minveclem3  24830  pmltpc  24851  ovolscalem2  24915  ovolicc2lem5  24922  ovolicc2  24923  nulmbl2  24937  ioombl1  24963  uniioombllem6  24989  uniioombl  24990  vitalilem3  25011  i1faddlem  25094  mbfmullem  25127  itg2const2  25143  itg2split  25151  lhop2  25416  dvfsumrlim  25432  itgsubst  25450  plydivex  25694  plyexmo  25710  ulmbdd  25794  cxploglim  26364  dchrptlem2  26650  lgsquad2lem2  26770  2sqlem5  26807  dchrvmasumif  26888  rpvmasum2  26897  dchrisum0re  26898  dchrisum0lem3  26904  dchrisum0  26905  dchrmusum  26909  dchrvmasum  26910  pntibndlem3  26977  pntlemp  26995  ostth3  27023  nosupbday  27090  nosupbnd1lem1  27093  nosupbnd2  27101  noinfbday  27105  noinfbnd1lem1  27108  noinfbnd2  27116  conway  27181  madebdaylemlrcut  27271  legtrid  27596  hlcgreu  27623  mirreu3  27659  opphllem  27740  oppperpex  27758  lnperpex  27808  trgcopy  27809  iscgra1  27815  cgraswap  27825  cgracom  27827  cgratr  27828  flatcgra  27829  acopyeu  27839  ax5seglem9  27949  ax5seg  27950  axcontlem8  27983  axcontlem12  27987  upgrclwlkcompim  28792  wwlksnextwrd  28905  2pthfrgr  29291  frgrnbnb  29300  ablo4  29555  smcnlem  29702  pjhthmo  30307  1stpreimas  31687  xrge0tsmsd  31969  locfinref  32511  xpinpreima2  32577  qqhval2  32652  dya2iocnrect  32970  orvcgteel  33156  orvclteel  33161  cnpconn  33911  txpconn  33913  connpconn  33916  pconnpi1  33918  iccllysconn  33931  rellysconn  33932  cvmcov2  33956  cvmliftmolem2  33963  cvmliftmo  33965  cvmliftlem15  33979  cvmliftpht  33999  cvmlift3lem2  34001  cgrextend  34669  btwnouttr2  34683  btwnexch2  34684  cgrxfr  34716  lineext  34737  btwnconn1lem5  34752  btwnconn1lem13  34760  btwnconn3  34764  segletr  34775  segleantisym  34776  outsideofeq  34791  outsidele  34793  lineunray  34808  refssfne  34906  neibastop2lem  34908  neibastop2  34909  unblimceq0lem  35045  knoppndvlem22  35072  mblfinlem3  36190  mblfinlem4  36191  cnambfre  36199  itg2addnclem  36202  areacirclem5  36243  istotbnd3  36303  crngm4  36535  cvlcvr1  37874  4atlem12  38148  cdlemb  38330  paddasslem10  38365  paddasslem12  38367  paddasslem13  38368  lhpexle3lem  38547  cdlemd4  38737  cdlemefs32sn1aw  38950  cdleme43fsv1snlem  38956  cdleme32d  38980  cdleme32f  38982  cdleme40m  39003  cdleme40n  39004  cdleme50trn2  39087  cdlemftr3  39101  cdlemm10N  39654  dihvalcqpre  39771  dihopelvalcpre  39784  dihmeetlem1N  39826  dihglblem5apreN  39827  dihmeetlem4preN  39842  dihjat1lem  39964  mapd0  40201  mapdh9a  40325  nna4b4nsq  41056  mzpmfp  41128  mzpcompact2lem  41132  diophin  41153  pellexlem3  41212  pellex  41216  pell14qrmulcl  41244  jm2.19lem3  41373  jm2.25  41381  jm2.27b  41388  fnwe2lem2  41436  hbtlem2  41509  hbtlem5  41513  gsumws3  42591  gsumws4  42592  mnuprdlem1  42674  mnuprdlem2  42675  mnuprdlem4  42677  fnchoice  43356  stoweidlem53  44414  stoweidlem61  44422  qndenserrnbllem  44655  bgoldbtbnd  46121  prsthinc  47194