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 484	. 2 ⊢ ((𝜑 ∧ 𝜏) → 𝜑)
2		adantl2.1	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
3	1, 2	sylanl1 679	1 ⊢ ((((𝜑 ∧ 𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  ad4ant13  750  ad4ant134  1175  ad5ant145  1370  oewordri  8592  marypha1lem  9428  rlimsqzlem  15595  fsumrlim  15757  fsumo1  15758  lcmdvds  16545  dfgrp3lem  18921  tgcl  22472  neindisj  22621  neiptoptop  22635  isr0  23241  cnextcn  23571  ustuqtop4  23749  mbfsup  25181  itg2i1fseqle  25272  ditgsplit  25378  itgulm  25920  leibpi  26447  dchrisumlem3  26994  legov  27836  legov2  27837  legtrid  27842  colopp  28020  f1otrg  28122  cusgrsize2inds  28710  grpoidinvlem3  29759  grpoideu  29762  grporcan  29771  blocni  30058  normcan  30829  unoplin  31173  hmoplin  31195  nmophmi  31284  mdslmd3i  31585  chirredlem1  31643  chirredlem2  31644  mdsymlem5  31660  cdj1i  31686  opreu2reuALT  31717  fpwrelmap  31958  fsumiunle  32035  ccatf1  32115  wrdt2ind  32117  archiabllem1  32339  archiabl  32344  isarchiofld  32435  ringlsmss1  32506  ringlsmss2  32507  nsgqusf1olem1  32524  nsgqusf1olem2  32525  nsgqusf1olem3  32526  rhmimaidl  32550  isprmidlc  32566  fedgmul  32716  irngnzply1  32755  locfinreflem  32820  pstmxmet  32877  ordtconnlem1  32904  esumcvg  33084  esum2d  33091  esumiun  33092  ldgenpisyslem1  33161  omssubadd  33299  signstfvneq0  33583  circlemeth  33652  mpomulcn  35162  elicc3  35202  knoppcnlem9  35377  pibt2  36298  lindsenlbs  36483  matunitlindflem1  36484  poimirlem17  36505  poimirlem20  36508  poimirlem27  36515  poimirlem29  36517  poimir  36521  heicant  36523  itg2addnclem  36539  ftc1anclem5  36565  ftc1anclem6  36566  ftc1anclem7  36567  ftc1anclem8  36568  ftc1anc  36569  fzmul  36609  fdc  36613  fdc1  36614  incsequz2  36617  rrncmslem  36700  ghomco  36759  rngoisocnv  36849  ispridlc  36938  selvvvval  41157  fsuppind  41162  cvgdvgrat  43072  binomcxplemnotnn0  43115  founiiun0  43888  supxrge  44048  suplesup  44049  supxrunb3  44109  lptre2pt  44356  0ellimcdiv  44365  limclner  44367  limsuppnfdlem  44417  limsuppnflem  44426  limsupmnflem  44436  liminfreuzlem  44518  liminflimsupclim  44523  cnrefiisplem  44545  climxlim2lem  44561  xlimliminflimsup  44578  icccncfext  44603  cncfiooiccre  44611  fperdvper  44635  dvnprodlem2  44663  iblcncfioo  44694  stoweidlem35  44751  wallispilem3  44783  fourierdlem20  44843  fourierdlem34  44857  fourierdlem39  44862  fourierdlem42  44865  fourierdlem46  44868  fourierdlem48  44870  fourierdlem49  44871  fourierdlem63  44885  fourierdlem64  44886  fourierdlem73  44895  fourierdlem87  44909  fourierdlem97  44919  fourierdlem103  44925  fourierdlem104  44926  fourierdlem111  44933  etransclem32  44982  etransclem33  44983  etransclem35  44985  sge0cl  45097  sge0f1o  45098  sge0split  45125  sge0iunmptlemre  45131  sge0rpcpnf  45137  sge0xadd  45151  nnfoctbdjlem  45171  ismeannd  45183  omeiunltfirp  45235  hoidmvlelem3  45313  hoidmvle  45316  ovncvr2  45327  hspdifhsp  45332  hspmbllem2  45343  ovnsubadd2lem  45361  pimdecfgtioo  45433  pimincfltioo  45434  smflimlem1  45487  smflimmpt  45526  smfpimne2  45556  aacllem  47848