Theorem ad4ant13 747

Description: Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)

Hypothesis

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

Assertion

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

Proof of Theorem ad4ant13

Step	Hyp	Ref	Expression
1		ad4ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantr 481	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜒)
3	2	adantllr 715	1 ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜓) ∧ 𝜏) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  ad5ant14  754  ad5ant24  757  fntpb  6838  peano5  7461  f1o2ndf1  7671  cantnfle  8980  cantnflem1c  8996  ttukeylem5  9781  rlimsqzlem  14839  dvdslcmf  15804  poslubmo  17585  posglbmo  17586  isgrpinv  17913  ghmgrp  17980  dprdfcntz  18854  cply1coe0bi  20151  isnrm3  21651  cnextcn  22359  ustexsym  22507  ustex2sym  22508  ustex3sym  22509  trust  22521  fmucnd  22584  trcfilu  22586  metust  22851  cxpmul2z  24955  umgrres1lem  26775  upgrres1  26778  friendshipgt3  27869  cyc3evpm  30430  repr0  31499  breprexplemc  31520  hgt750lemb  31544  satffunlem1lem2  32258  satffunlem2lem2  32261  lindsadd  34416  matunitlindflem1  34419  mapss2  41008  supxrge  41147  xrlexaddrp  41161  infxr  41176  infleinf  41181  unb2ltle  41231  supminfxr  41282  limsuppnfdlem  41524  limsupub  41527  limsuppnflem  41533  climinf3  41539  limsupmnflem  41543  climxrre  41573  liminfvalxr  41606  fperdvper  41744  sge0isum  42251  sge0gtfsumgt  42267  sge0seq  42270  nnfoctbdjlem  42279  meaiuninc3v  42308  omeiunltfirp  42343  hspdifhsp  42440  hspmbllem2  42451  pimdecfgtioo  42537  pimincfltioo  42538  preimageiingt  42540  preimaleiinlt  42541  smfid  42571  proththd  43261