Theorem ad4ant24 1298

Description: Deduction adding conjuncts to antecedent. (Contributed by Alan Sare, 17-Oct-2017.)

Hypothesis

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

Assertion

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

Proof of Theorem ad4ant24

Step	Hyp	Ref	Expression
1		ad4ant24.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 450	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	a1i13 27	. 2 ⊢ (𝜃 → (𝜑 → (𝜏 → (𝜓 → 𝜒))))
4	3	imp41 619	1 ⊢ ((((𝜃 ∧ 𝜑) ∧ 𝜏) ∧ 𝜓) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 384

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 386

This theorem is referenced by:  seqshft  13825  numclwlk1lem2f1  27227  matunitlindflem1  33405  matunitlindflem2  33406  founiiun0  39377  xralrple2  39570  rexabslelem  39645  climisp  39978  climxrre  39982  cnrefiisplem  40055  sge0iunmptlemre  40632  nnfoctbdjlem  40672  iundjiun  40677  hoidmvlelem3  40811  hspmbllem2  40841  smflimlem2  40980