Theorem 3adant2l 1175

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) (Proof shortened by Wolf Lammen, 25-Jun-2022.)

Hypothesis

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

Assertion

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

Proof of Theorem 3adant2l

Step	Hyp	Ref	Expression
1		simpr 483	. 2 ⊢ ((𝜏 ∧ 𝜓) → 𝜓)
2		ad4ant3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	syl3an2 1161	1 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  axdc3lem4  10487  modexp  14250  lmmbr2  25275  ax5seglem1  28859  ax5seglem2  28860  nvaddsub4  30587  pl1cn  33783  athgt  39168  ltrncoelN  39855  ltrncoat  39856  trlcoabs  40433  tendoplcl2  40490  tendopltp  40492  dih1dimatlem0  41040  pellex  42529  fourierdlem42  45806