Theorem adantllr 720

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)

Hypothesis

Ref	Expression
adantl2.1	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
adantllr	⊢ ((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem adantllr

Step	Hyp	Ref	Expression
1		simpl 482	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜑)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl1 681	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:  ad4ant13  752  ad4ant134  1176  ad5ant145  1372  oewordri  8528  marypha1lem  9346  rlimsqzlem  15611  fsumrlim  15774  fsumo1  15775  lcmdvds  16577  chnind  18587  dfgrp3lem  19014  tgcl  22934  neindisj  23082  neiptoptop  23096  isr0  23702  cnextcn  24032  ustuqtop4  24209  mpomulcn  24834  mbfsup  25631  itg2i1fseqle  25721  ditgsplit  25828  itgulm  26373  leibpi  26906  dchrisumlem3  27454  legov  28653  legov2  28654  legtrid  28659  colopp  28837  f1otrg  28939  cusgrsize2inds  29522  grpoidinvlem3  30577  grpoideu  30580  grporcan  30589  blocni  30876  normcan  31647  unoplin  31991  hmoplin  32013  nmophmi  32102  mdslmd3i  32403  chirredlem1  32461  chirredlem2  32462  mdsymlem5  32478  cdj1i  32504  opreu2reuALT  32546  fpwrelmap  32806  fsumiunle  32902  ccatf1  33009  wrdt2ind  33013  suppgsumssiun  33133  gsumwrd2dccatlem  33138  archiabllem1  33254  archiabl  33259  isarchiofld  33260  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem4  33306  elrgspnsubrunlem2  33309  ringlsmss1  33456  ringlsmss2  33457  nsgqusf1olem1  33473  nsgqusf1olem2  33474  nsgqusf1olem3  33475  rhmimaidl  33492  isprmidlc  33507  mplvrpmrhm  33691  esplyfv1  33713  esplyfval1  33717  fedgmul  33775  irngnzply1  33835  locfinreflem  33984  pstmxmet  34041  ordtconnlem1  34068  esumcvg  34230  esum2d  34237  esumiun  34238  ldgenpisyslem1  34307  omssubadd  34444  signstfvneq0  34716  circlemeth  34784  elicc3  36499  knoppcnlem9  36761  pibt2  37733  lindsenlbs  37936  matunitlindflem1  37937  poimirlem17  37958  poimirlem20  37961  poimirlem27  37968  poimirlem29  37970  poimir  37974  heicant  37976  itg2addnclem  37992  ftc1anclem5  38018  ftc1anclem6  38019  ftc1anclem7  38020  ftc1anclem8  38021  ftc1anc  38022  fzmul  38062  fdc  38066  fdc1  38067  incsequz2  38070  rrncmslem  38153  ghomco  38212  rngoisocnv  38302  ispridlc  38391  fiabv  42981  selvvvval  43018  fsuppind  43023  cvgdvgrat  44740  binomcxplemnotnn0  44783  founiiun0  45620  supxrge  45768  suplesup  45769  supxrunb3  45828  lptre2pt  46068  0ellimcdiv  46077  limclner  46079  limsuppnfdlem  46129  limsuppnflem  46138  limsupmnflem  46148  liminfreuzlem  46230  liminflimsupclim  46235  cnrefiisplem  46257  climxlim2lem  46273  xlimliminflimsup  46290  icccncfext  46315  cncfiooiccre  46323  fperdvper  46347  dvnprodlem2  46375  iblcncfioo  46406  stoweidlem35  46463  wallispilem3  46495  fourierdlem20  46555  fourierdlem34  46569  fourierdlem39  46574  fourierdlem42  46577  fourierdlem46  46580  fourierdlem48  46582  fourierdlem49  46583  fourierdlem63  46597  fourierdlem64  46598  fourierdlem73  46607  fourierdlem87  46621  fourierdlem97  46631  fourierdlem103  46637  fourierdlem104  46638  fourierdlem111  46645  etransclem32  46694  etransclem33  46695  etransclem35  46697  sge0cl  46809  sge0f1o  46810  sge0split  46837  sge0iunmptlemre  46843  sge0rpcpnf  46849  sge0xadd  46863  nnfoctbdjlem  46883  ismeannd  46895  omeiunltfirp  46947  hoidmvlelem3  47025  hoidmvle  47028  ovncvr2  47039  hspdifhsp  47044  hspmbllem2  47055  ovnsubadd2lem  47073  pimdecfgtioo  47145  pimincfltioo  47146  smflimlem1  47199  smflimmpt  47238  smfpimne2  47268  resccat  49549  aacllem  50276