Theorem ad4ant13 758

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

Syntax hints:   → wi 4   ∧ wa 385

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 199  df-an 386

This theorem is referenced by:  ad5ant14  770  ad5ant24  776  fntpb  6701  dvdslcmf  15676  poslubmo  17458  posglbmo  17459  trust  22358  metust  22688  umgrres1lem  26537  upgrres1  26540  friendshipgt3  27776  repr0  31202  breprexplemc  31223  hgt750lemb  31247  matunitlindflem1  33887  mapss2  40138  supxrge  40287  xrlexaddrp  40301  infxr  40316  infleinf  40321  unb2ltle  40374  supminfxr  40426  limsuppnfdlem  40666  limsupub  40669  limsuppnflem  40675  climinf3  40681  limsupmnflem  40685  climxrre  40715  liminfvalxr  40748  fperdvper  40866  sge0isum  41376  sge0gtfsumgt  41392  sge0seq  41395  nnfoctbdjlem  41404  meaiuninc3v  41433  omeiunltfirp  41468  hspdifhsp  41565  hspmbllem2  41576  pimdecfgtioo  41662  pimincfltioo  41663  preimageiingt  41665  preimaleiinlt  41666  smfid  41696  proththd  42302