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  7213  peano5  7886  peano5OLD  7887  f1o2ndf1  8110  cantnfle  9668  cantnflem1c  9684  ttukeylem5  10510  rlimsqzlem  15599  dvdslcmf  16572  poslubmo  18368  posglbmo  18369  smndex1mgm  18824  isgrpinv  18914  ghmgrp  18985  dprdfcntz  19926  pzriprnglem4  21253  sraassab  21641  cply1coe0bi  22044  isnrm3  23083  cnextcn  23791  ustexsym  23940  ustex2sym  23941  ustex3sym  23942  trust  23954  fmucnd  24017  trcfilu  24019  metust  24287  cxpmul2z  26423  umgrres1lem  28822  upgrres1  28825  friendshipgt3  29906  ccatf1  32370  cyc3evpm  32567  znfermltl  32741  rhmimaidl  32812  evls1fpws  32908  txomap  33100  zart0  33145  repr0  33909  breprexplemc  33930  hgt750lemb  33954  satffunlem1lem2  34680  satffunlem2lem2  34683  lindsadd  36784  matunitlindflem1  36787  nadd1suc  42444  mapss2  44203  supxrge  44347  xrlexaddrp  44361  infxr  44376  infleinf  44381  unb2ltle  44424  supminfxr  44473  limsuppnfdlem  44716  limsupub  44719  limsuppnflem  44725  climinf3  44731  limsupmnflem  44735  climxrre  44765  liminfvalxr  44798  fperdvper  44934  sge0isum  45442  sge0gtfsumgt  45458  sge0seq  45461  nnfoctbdjlem  45470  meaiuninc3v  45499  omeiunltfirp  45534  hspdifhsp  45631  hspmbllem2  45642  pimdecfgtioo  45732  pimincfltioo  45733  preimageiingt  45735  preimaleiinlt  45736  smfid  45767  proththd  46581