Theorem adantllr 718

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 679	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  750  ad4ant134  1174  ad5ant145  1369  oewordri  8648  marypha1lem  9502  rlimsqzlem  15697  fsumrlim  15859  fsumo1  15860  lcmdvds  16655  dfgrp3lem  19078  tgcl  22997  neindisj  23146  neiptoptop  23160  isr0  23766  cnextcn  24096  ustuqtop4  24274  mpomulcn  24910  mbfsup  25718  itg2i1fseqle  25809  ditgsplit  25916  itgulm  26469  leibpi  27003  dchrisumlem3  27553  legov  28611  legov2  28612  legtrid  28617  colopp  28795  f1otrg  28897  cusgrsize2inds  29489  grpoidinvlem3  30538  grpoideu  30541  grporcan  30550  blocni  30837  normcan  31608  unoplin  31952  hmoplin  31974  nmophmi  32063  mdslmd3i  32364  chirredlem1  32422  chirredlem2  32423  mdsymlem5  32439  cdj1i  32465  opreu2reuALT  32505  fpwrelmap  32747  fsumiunle  32833  ccatf1  32915  wrdt2ind  32920  chnind  32983  archiabllem1  33173  archiabl  33178  isarchiofld  33312  ringlsmss1  33389  ringlsmss2  33390  nsgqusf1olem1  33406  nsgqusf1olem2  33407  nsgqusf1olem3  33408  rhmimaidl  33425  isprmidlc  33440  fedgmul  33644  irngnzply1  33691  locfinreflem  33786  pstmxmet  33843  ordtconnlem1  33870  esumcvg  34050  esum2d  34057  esumiun  34058  ldgenpisyslem1  34127  omssubadd  34265  signstfvneq0  34549  circlemeth  34617  elicc3  36283  knoppcnlem9  36467  pibt2  37383  lindsenlbs  37575  matunitlindflem1  37576  poimirlem17  37597  poimirlem20  37600  poimirlem27  37607  poimirlem29  37609  poimir  37613  heicant  37615  itg2addnclem  37631  ftc1anclem5  37657  ftc1anclem6  37658  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  fzmul  37701  fdc  37705  fdc1  37706  incsequz2  37709  rrncmslem  37792  ghomco  37851  rngoisocnv  37941  ispridlc  38030  fiabv  42491  selvvvval  42540  fsuppind  42545  cvgdvgrat  44282  binomcxplemnotnn0  44325  founiiun0  45097  supxrge  45253  suplesup  45254  supxrunb3  45314  lptre2pt  45561  0ellimcdiv  45570  limclner  45572  limsuppnfdlem  45622  limsuppnflem  45631  limsupmnflem  45641  liminfreuzlem  45723  liminflimsupclim  45728  cnrefiisplem  45750  climxlim2lem  45766  xlimliminflimsup  45783  icccncfext  45808  cncfiooiccre  45816  fperdvper  45840  dvnprodlem2  45868  iblcncfioo  45899  stoweidlem35  45956  wallispilem3  45988  fourierdlem20  46048  fourierdlem34  46062  fourierdlem39  46067  fourierdlem42  46070  fourierdlem46  46073  fourierdlem48  46075  fourierdlem49  46076  fourierdlem63  46090  fourierdlem64  46091  fourierdlem73  46100  fourierdlem87  46114  fourierdlem97  46124  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  etransclem32  46187  etransclem33  46188  etransclem35  46190  sge0cl  46302  sge0f1o  46303  sge0split  46330  sge0iunmptlemre  46336  sge0rpcpnf  46342  sge0xadd  46356  nnfoctbdjlem  46376  ismeannd  46388  omeiunltfirp  46440  hoidmvlelem3  46518  hoidmvle  46521  ovncvr2  46532  hspdifhsp  46537  hspmbllem2  46548  ovnsubadd2lem  46566  pimdecfgtioo  46638  pimincfltioo  46639  smflimlem1  46692  smflimmpt  46731  smfpimne2  46761  aacllem  48895