Theorem ad4ant13 749

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 717	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 206  df-an 397

This theorem is referenced by:  ad5ant14  756  ad5ant24  759  fntpb  7164  peano5  7835  peano5OLD  7836  f1o2ndf1  8059  cantnfle  9616  cantnflem1c  9632  ttukeylem5  10458  rlimsqzlem  15545  dvdslcmf  16518  poslubmo  18314  posglbmo  18315  smndex1mgm  18731  isgrpinv  18818  ghmgrp  18885  dprdfcntz  19808  cply1coe0bi  21708  isnrm3  22747  cnextcn  23455  ustexsym  23604  ustex2sym  23605  ustex3sym  23606  trust  23618  fmucnd  23681  trcfilu  23683  metust  23951  cxpmul2z  26083  umgrres1lem  28321  upgrres1  28324  friendshipgt3  29405  ccatf1  31875  cyc3evpm  32069  znfermltl  32227  rhmimaidl  32282  evls1fpws  32348  txomap  32504  zart0  32549  repr0  33313  breprexplemc  33334  hgt750lemb  33358  satffunlem1lem2  34084  satffunlem2lem2  34087  lindsadd  36144  matunitlindflem1  36147  nadd1suc  41785  mapss2  43547  supxrge  43693  xrlexaddrp  43707  infxr  43722  infleinf  43727  unb2ltle  43770  supminfxr  43819  limsuppnfdlem  44062  limsupub  44065  limsuppnflem  44071  climinf3  44077  limsupmnflem  44081  climxrre  44111  liminfvalxr  44144  fperdvper  44280  sge0isum  44788  sge0gtfsumgt  44804  sge0seq  44807  nnfoctbdjlem  44816  meaiuninc3v  44845  omeiunltfirp  44880  hspdifhsp  44977  hspmbllem2  44988  pimdecfgtioo  45078  pimincfltioo  45079  preimageiingt  45081  preimaleiinlt  45082  smfid  45113  proththd  45926