Theorem ad4ant23 766

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
ad4ant23	⊢ ((((𝜃 ∧ 𝜑) ∧ 𝜓) ∧ 𝜏) → 𝜒)

Proof of Theorem ad4ant23

Step	Hyp	Ref	Expression
1		ad4ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantr 486	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜏) → 𝜒)
3	2	adantlll 731	1 ⊢ ((((𝜃 ∧ 𝜑) ∧ 𝜓) ∧ 𝜏) → 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  fntpb  7214  suppssfv  8204  omsmolem  8649  ttukeylem5  10512  rlim3  15573  mp2pm2mplem4  23016  chfacfisf  23061  chfacfisfcpmat  23062  mbfi1fseqlem3  25927  usgredg2vlem2  29634  umgr3v3e3cycl  30606  zringfrac  33908  matunitlindflem1  38324  matunitlindflem2  38325  heicant  38363  naddgeoa  44179  difmap  45981  xlimmnfvlem2  46605  xlimpnfvlem2  46609  xlimliminflimsup  46634  sge0resplit  47178  hoidmvle  47372  grimcnv  48711  eenglngeehlnmlem2  49575