Theorem ad4ant13 1207

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	adantlr 753	. 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)
3	2	adantr 472	1 ⊢ ((((𝜑 ∧ 𝜃) ∧ 𝜓) ∧ 𝜏) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 383

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 197  df-an 385

This theorem is referenced by:  ad5ant14  1218  ad5ant24  1224  fntpb  6638  dvdslcmf  15566  poslubmo  17367  posglbmo  17368  trust  22254  metust  22584  umgrres1lem  26422  upgrres1  26425  friendshipgt3  27587  repr0  31019  breprexplemc  31040  hgt750lemb  31064  matunitlindflem1  33736  mapss2  39914  supxrge  40070  xrlexaddrp  40084  infxr  40099  infleinf  40104  unb2ltle  40158  supminfxr  40210  limsuppnfdlem  40454  limsupub  40457  limsuppnflem  40463  climinf3  40469  limsupmnflem  40473  climxrre  40503  liminfvalxr  40536  sge0isum  41165  sge0gtfsumgt  41181  sge0seq  41184  nnfoctbdjlem  41193  meaiuninc3v  41222  omeiunltfirp  41257  hspdifhsp  41354  hspmbllem2  41365  pimdecfgtioo  41451  pimincfltioo  41452  preimageiingt  41454  preimaleiinlt  41455  smfid  41485  proththd  42059