Theorem 3adant2r 1180

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

Proof of Theorem 3adant2r

Step	Hyp	Ref	Expression
1		simpl 482	. 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓)
2		ad4ant3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	syl3an2 1164	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  ltdiv23  12138  lediv23  12139  divalglem8  16424  isdrngd  20730  isdrngdOLD  20732  deg1tm  26081  ax5seglem1  28912  ax5seglem2  28913  nvaddsub4  30643  nmoub2i  30760  cdleme21at  40352  cdleme42f  40504  trlcoabs2N  40746  tendoplcl2  40802  tendopltp  40804  cdlemk2  40856  cdlemk8  40862  cdlemk9  40863  cdlemk9bN  40864  cdleml8  41007  dihglblem3N  41319  dihglblem3aN  41320  fourierdlem42  46145  lincscm  48373  itsclc0yqsol  48711