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  4855  f1prex  7213  fliftfun  7241  fprresex  8235  nnaordex2  8549  naddssim  8595  mapdom2  9056  domunfican  9201  fofinf1o  9211  finsschain  9238  wemaplem3  9429  oemapvali  9569  iunfictbso  9997  enfin2i  10204  fin1a2s  10297  distrlem4pr  10909  mulcmpblnr  10954  prsrlem1  10955  addsrmo  10956  mulsrmo  10957  divdivdiv  11814  divsubdiv  11829  lediv12a  12007  xralrple  13096  seqcaopr  13938  leexp2r  14073  hashbclem  14351  wrd2ind  14622  cshwidxmod  14702  rtrclreclem4  14960  relexpindlem  14962  rtrclind  14964  rlimresb  15464  summo  15616  fsum2dlem  15669  prodmo  15835  fprod2dlem  15879  bezoutlem3  16444  bezoutlem4  16445  qredeu  16561  coprmproddvdslem  16565  prmdvdsncoprmbd  16630  pcqmul  16757  pcadd  16793  pockthg  16810  ramub1lem2  16931  cshwsdisj  17002  mreexexlem4d  17545  issubc3  17748  cofucl  17787  setcmon  17986  setcepi  17987  drsdirfi  18203  poslubmo  18307  posglbmo  18308  grprida  18575  ghmpreima  19143  gaorber  19213  psgnunilem4  19402  psgneu  19411  odcau  19509  pgpssslw  19519  fislw  19530  lsmsubm  19558  efgsfo  19644  pgpfac1  19987  pgpfaclem2  19989  pgpfaclem3  19990  unitgrp  20294  islmodd  20792  lmodprop2d  20850  lsspropd  20944  lbsextlem4  21091  assapropd  21802  evlslem1  22010  mdetunilem8  22527  mdetmul  22531  ppttop  22915  epttop  22917  restbas  23066  iscnp4  23171  cnpco  23175  nrmsep  23265  regsep2  23284  ordthauslem  23291  1stcfb  23353  2ndcctbss  23363  2ndcdisj  23364  2ndcomap  23366  dis2ndc  23368  1stcelcls  23369  nlly2i  23384  islly2  23392  hausllycmp  23402  lly1stc  23404  comppfsc  23440  1stckgenlem  23461  ptbasin  23485  txcls  23512  ptcnp  23530  txlly  23544  txnlly  23545  txtube  23548  txcmplem1  23549  txcmplem2  23550  xkococnlem  23567  basqtop  23619  regr1lem  23647  kqreglem1  23649  kqreglem2  23650  kqnrmlem1  23651  kqnrmlem2  23652  reghmph  23701  nrmhmph  23702  filuni  23793  rnelfmlem  23860  fmufil  23867  fclscf  23933  fclsfnflim  23935  flimfnfcls  23936  uffclsflim  23939  cnpfcfi  23948  cnpfcf  23949  alexsublem  23952  alexsubALTlem3  23957  tgpconncompeqg  24020  ghmcnp  24023  qustgplem  24029  blssps  24332  blss  24333  blcld  24413  metequiv2  24418  met2ndci  24430  prdsxmslem2  24437  txmetcnp  24455  nlmvscnlem1  24594  xrge0tsms  24743  ipcnlem1  25165  iscmet3  25213  metsscmetcld  25235  minveclem3  25349  pmltpc  25371  ovolscalem2  25435  ovolicc2lem5  25442  ovolicc2  25443  nulmbl2  25457  ioombl1  25483  uniioombllem6  25509  uniioombl  25510  vitalilem3  25531  i1faddlem  25614  mbfmullem  25646  itg2const2  25662  itg2split  25670  lhop2  25940  dvfsumrlim  25958  itgsubst  25976  plydivex  26225  plyexmo  26241  ulmbdd  26327  cxploglim  26908  dchrptlem2  27196  lgsquad2lem2  27316  2sqlem5  27353  dchrvmasumif  27434  rpvmasum2  27443  dchrisum0re  27444  dchrisum0lem3  27450  dchrisum0  27451  dchrmusum  27455  dchrvmasum  27456  pntibndlem3  27523  pntlemp  27541  ostth3  27569  nosupbday  27637  nosupbnd1lem1  27640  nosupbnd2  27648  noinfbday  27652  noinfbnd1lem1  27655  noinfbnd2  27663  conway  27733  madebdaylemlrcut  27837  mulsproplem9  28056  mulsuniflem  28081  uzsind  28322  readdscl  28394  legtrid  28562  hlcgreu  28589  mirreu3  28625  opphllem  28706  oppperpex  28724  lnperpex  28774  trgcopy  28775  iscgra1  28781  cgraswap  28791  cgracom  28793  cgratr  28794  flatcgra  28795  acopyeu  28805  ax5seglem9  28908  ax5seg  28909  axcontlem8  28942  axcontlem12  28946  upgrclwlkcompim  29752  wwlksnextwrd  29868  2pthfrgr  30254  frgrnbnb  30263  ablo4  30520  smcnlem  30667  pjhthmo  31272  1stpreimas  32677  xrge0tsmsd  33032  locfinref  33844  xpinpreima2  33910  qqhval2  33985  dya2iocnrect  34284  orvcgteel  34471  orvclteel  34476  cnpconn  35242  txpconn  35244  connpconn  35247  pconnpi1  35249  iccllysconn  35262  rellysconn  35263  cvmcov2  35287  cvmliftmolem2  35294  cvmliftmo  35296  cvmliftlem15  35310  cvmliftpht  35330  cvmlift3lem2  35332  cgrextend  36021  btwnouttr2  36035  btwnexch2  36036  cgrxfr  36068  lineext  36089  btwnconn1lem5  36104  btwnconn1lem13  36112  btwnconn3  36116  segletr  36127  segleantisym  36128  outsideofeq  36143  outsidele  36145  lineunray  36160  refssfne  36371  neibastop2lem  36373  neibastop2  36374  weiunpo  36478  unblimceq0lem  36519  knoppndvlem22  36546  mblfinlem3  37678  mblfinlem4  37679  cnambfre  37687  itg2addnclem  37690  areacirclem5  37731  istotbnd3  37790  crngm4  38022  cvlcvr1  39357  4atlem12  39630  cdlemb  39812  paddasslem10  39847  paddasslem12  39849  paddasslem13  39850  lhpexle3lem  40029  cdlemd4  40219  cdlemefs32sn1aw  40432  cdleme43fsv1snlem  40438  cdleme32d  40462  cdleme32f  40464  cdleme40m  40485  cdleme40n  40486  cdleme50trn2  40569  cdlemftr3  40583  cdlemm10N  41136  dihvalcqpre  41253  dihopelvalcpre  41266  dihmeetlem1N  41308  dihglblem5apreN  41309  dihmeetlem4preN  41324  dihjat1lem  41446  mapd0  41683  mapdh9a  41807  nna4b4nsq  42672  mzpmfp  42759  mzpcompact2lem  42763  diophin  42784  pellexlem3  42843  pellex  42847  pell14qrmulcl  42875  jm2.19lem3  43003  jm2.25  43011  jm2.27b  43018  fnwe2lem2  43063  hbtlem2  43136  hbtlem5  43140  gsumws3  44208  gsumws4  44209  mnuprdlem1  44284  mnuprdlem2  44285  mnuprdlem4  44287  fnchoice  45045  stoweidlem53  46070  stoweidlem61  46078  qndenserrnbllem  46311  bgoldbtbnd  47819  cycldlenngric  47938  grtrimap  47958  isubgr3stgrlem6  47981  prsthinc  49475