Theorem ad4ant13 748

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 716	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  755  ad5ant24  758  fntpb  7085  peano5  7740  peano5OLD  7741  f1o2ndf1  7963  cantnfle  9429  cantnflem1c  9445  ttukeylem5  10269  rlimsqzlem  15360  dvdslcmf  16336  poslubmo  18129  posglbmo  18130  smndex1mgm  18546  isgrpinv  18632  ghmgrp  18699  dprdfcntz  19618  cply1coe0bi  21471  isnrm3  22510  cnextcn  23218  ustexsym  23367  ustex2sym  23368  ustex3sym  23369  trust  23381  fmucnd  23444  trcfilu  23446  metust  23714  cxpmul2z  25846  umgrres1lem  27677  upgrres1  27680  friendshipgt3  28762  ccatf1  31223  cyc3evpm  31417  znfermltl  31562  rhmimaidl  31609  txomap  31784  zart0  31829  repr0  32591  breprexplemc  32612  hgt750lemb  32636  satffunlem1lem2  33365  satffunlem2lem2  33368  lindsadd  35770  matunitlindflem1  35773  mapss2  42745  supxrge  42877  xrlexaddrp  42891  infxr  42906  infleinf  42911  unb2ltle  42955  supminfxr  43004  limsuppnfdlem  43242  limsupub  43245  limsuppnflem  43251  climinf3  43257  limsupmnflem  43261  climxrre  43291  liminfvalxr  43324  fperdvper  43460  sge0isum  43965  sge0gtfsumgt  43981  sge0seq  43984  nnfoctbdjlem  43993  meaiuninc3v  44022  omeiunltfirp  44057  hspdifhsp  44154  hspmbllem2  44165  pimdecfgtioo  44254  pimincfltioo  44255  preimageiingt  44257  preimaleiinlt  44258  smfid  44288  proththd  45066