Theorem adantllr 732

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  ad4ant13  764  ad4ant134  1193  ad5ant145  1396  oewordri  8605  marypha1lem  9429  ccatf1  14740  rlimsqzlem  15822  fsumrlim  15984  fsumo1  15985  lcmdvds  16789  chnind  18801  dfgrp3lem  19254  isprmidlc  21634  lindsenlbs  22163  selvvvval  22457  matunitlindflem1  23000  tgcl  23293  neindisj  23441  neiptoptop  23455  isr0  24062  cnextcn  24392  ustuqtop4  24569  mpomulcn  25194  mbfsup  25991  itg2i1fseqle  26081  ditgsplit  26187  itgulm  26741  leibpi  27276  dchrisumlem3  27824  legov  29054  legov2  29055  legtrid  29060  colopp  29253  perpprlng  29434  f1otrg  29454  cusgrsize2inds  30040  grpoidinvlem3  31114  grpoideu  31117  grporcan  31126  blocni  31413  normcan  32184  unoplin  32528  hmoplin  32550  nmophmi  32639  mdslmd3i  32940  chirredlem1  32998  chirredlem2  32999  mdsymlem5  33015  cdj1i  33041  opreu2reuALT  33121  fpwrelmap  33372  fsumiunle  33467  wrdt2ind  33563  suppgsumssiun  33680  gsumwrd2dccatlem  33685  archiabllem1  33801  archiabl  33806  isarchiofld  33807  elrgspnlem1  33850  elrgspnlem2  33851  elrgspnlem4  33853  elrgspnsubrunlem2  33856  ringlsmss1  33996  ringlsmss2  33997  nsgqusf1olem1  34011  nsgqusf1olem2  34012  nsgqusf1olem3  34013  rhmimaidl  34029  mplvrpmrhm  34226  esplyfv1  34248  esplyfval1  34252  fedgmul  34310  irngnzply1  34370  locfinreflem  34519  pstmxmet  34576  ordtconnlem1  34603  esumcvg  34765  esum2d  34772  esumiun  34773  ldgenpisyslem1  34843  omssubadd  34979  signstfvneq0  35248  circlemeth  35316  elicc3  37198  knoppcnlem9  37460  pibt2  38434  poimirlem17  38649  poimirlem20  38652  poimirlem27  38659  poimirlem29  38661  poimir  38665  heicant  38667  itg2addnclem  38683  ftc1anclem5  38709  ftc1anclem6  38710  ftc1anclem7  38711  ftc1anclem8  38712  ftc1anc  38713  fzmul  38769  fdc  38773  fdc1  38774  incsequz2  38777  rrncmslem  38860  ghomco  38919  rngoisocnv  39009  ispridlc  39098  fiabv  43694  fsuppind  43712  cvgdvgrat  45391  binomcxplemnotnn0  45434  founiiun0  46299  supxrge  46444  suplesup  46445  supxrunb3  46504  lptre2pt  46744  0ellimcdiv  46753  limclner  46755  limsuppnfdlem  46805  limsuppnflem  46814  limsupmnflem  46824  liminfreuzlem  46906  liminflimsupclim  46911  cnrefiisplem  46933  climxlim2lem  46949  xlimliminflimsup  46966  icccncfext  46991  cncfiooiccre  46999  fperdvper  47023  dvnprodlem2  47051  iblcncfioo  47082  stoweidlem35  47139  wallispilem3  47171  fourierdlem20  47231  fourierdlem34  47245  fourierdlem39  47250  fourierdlem42  47253  fourierdlem46  47256  fourierdlem48  47258  fourierdlem49  47259  fourierdlem63  47273  fourierdlem64  47274  fourierdlem73  47283  fourierdlem87  47297  fourierdlem97  47307  fourierdlem103  47313  fourierdlem104  47314  fourierdlem111  47321  etransclem32  47370  etransclem33  47371  etransclem35  47373  sge0cl  47485  sge0f1o  47486  sge0split  47513  sge0iunmptlemre  47519  sge0rpcpnf  47525  sge0xadd  47539  nnfoctbdjlem  47559  ismeannd  47571  omeiunltfirp  47623  hoidmvlelem3  47701  hoidmvle  47704  ovncvr2  47715  hspdifhsp  47720  hspmbllem2  47731  ovnsubadd2lem  47749  pimdecfgtioo  47821  pimincfltioo  47822  smflimlem1  47875  smflimmpt  47914  smfpimne2  47944  resccat  50282  aacllem  51108