Theorem ad4ant13 750

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 480	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜒)
3	2	adantllr 718	1 ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜓) ∧ 𝜏) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  ad5ant14  757  ad5ant24  760  fntpb  7246  peano5  7932  peano5OLD  7933  f1o2ndf1  8163  cantnfle  9740  cantnflem1c  9756  ttukeylem5  10582  rlimsqzlem  15697  dvdslcmf  16678  poslubmo  18481  posglbmo  18482  smndex1mgm  18942  isgrpinv  19033  ghmgrp  19106  dprdfcntz  20059  pzriprnglem4  21518  sraassab  21911  cply1coe0bi  22327  evls1fpws  22394  isnrm3  23388  cnextcn  24096  ustexsym  24245  ustex2sym  24246  ustex3sym  24247  trust  24259  fmucnd  24322  trcfilu  24324  metust  24592  cxpmul2z  26751  umgrres1lem  29345  upgrres1  29348  friendshipgt3  30430  ccatf1  32915  cyc3evpm  33143  znfermltl  33359  rhmimaidl  33425  dimlssid  33645  txomap  33780  zart0  33825  repr0  34588  breprexplemc  34609  hgt750lemb  34633  satffunlem1lem2  35371  satffunlem2lem2  35374  lindsadd  37573  matunitlindflem1  37576  nadd1suc  43354  mapss2  45112  supxrge  45253  xrlexaddrp  45267  infxr  45282  infleinf  45287  unb2ltle  45330  supminfxr  45379  limsuppnfdlem  45622  limsupub  45625  limsuppnflem  45631  climinf3  45637  limsupmnflem  45641  climxrre  45671  liminfvalxr  45704  fperdvper  45840  sge0isum  46348  sge0gtfsumgt  46364  sge0seq  46367  nnfoctbdjlem  46376  meaiuninc3v  46405  omeiunltfirp  46440  hspdifhsp  46537  hspmbllem2  46548  pimdecfgtioo  46638  pimincfltioo  46639  preimageiingt  46641  preimaleiinlt  46642  smfid  46673  proththd  47488