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 480	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜒)
3	2	adantllr 715	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 206  df-an 396

This theorem is referenced by:  ad5ant14  754  ad5ant24  757  fntpb  7067  peano5  7714  peano5OLD  7715  f1o2ndf1  7934  cantnfle  9359  cantnflem1c  9375  ttukeylem5  10200  rlimsqzlem  15288  dvdslcmf  16264  poslubmo  18044  posglbmo  18045  smndex1mgm  18461  isgrpinv  18547  ghmgrp  18614  dprdfcntz  19533  cply1coe0bi  21381  isnrm3  22418  cnextcn  23126  ustexsym  23275  ustex2sym  23276  ustex3sym  23277  trust  23289  fmucnd  23352  trcfilu  23354  metust  23620  cxpmul2z  25751  umgrres1lem  27580  upgrres1  27583  friendshipgt3  28663  ccatf1  31125  cyc3evpm  31319  znfermltl  31464  rhmimaidl  31511  txomap  31686  zart0  31731  repr0  32491  breprexplemc  32512  hgt750lemb  32536  satffunlem1lem2  33265  satffunlem2lem2  33268  lindsadd  35697  matunitlindflem1  35700  mapss2  42634  supxrge  42767  xrlexaddrp  42781  infxr  42796  infleinf  42801  unb2ltle  42845  supminfxr  42894  limsuppnfdlem  43132  limsupub  43135  limsuppnflem  43141  climinf3  43147  limsupmnflem  43151  climxrre  43181  liminfvalxr  43214  fperdvper  43350  sge0isum  43855  sge0gtfsumgt  43871  sge0seq  43874  nnfoctbdjlem  43883  meaiuninc3v  43912  omeiunltfirp  43947  hspdifhsp  44044  hspmbllem2  44055  pimdecfgtioo  44141  pimincfltioo  44142  preimageiingt  44144  preimaleiinlt  44145  smfid  44175  proththd  44954