Theorem ad5ant15 756

Description: Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.) (Proof shortened by Wolf Lammen, 14-Apr-2022.)

Hypothesis

Ref	Expression
ad5ant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
ad5ant15	⊢ (((((𝜑 ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜓) → 𝜒)

Proof of Theorem ad5ant15

Step	Hyp	Ref	Expression
1		ad5ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantlr 712	. 2 ⊢ (((𝜑 ∧ 𝜃) ∧ 𝜓) → 𝜒)
3	2	ad4ant14 749	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:  summolem2  15428  ntrivcvg  15609  xkoccn  22770  abelthlem8  25598  rpvmasum2  26660  mulog2sumlem2  26683  f1otrge  27233  nn0xmulclb  31094  intlidl  31602  fedgmul  31712  signstfvneq0  32551  breprexplemc  32612  mblfinlem2  35815  supxrgelem  42876  supxrge  42877  rexabslelem  42958  uzub  42971  smflimlem4  44309