Theorem 3adant2r 1178

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 483	. 2 ⊢ ((𝜓 ∧ 𝜏) → 𝜓)
2		ad4ant3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	syl3an2 1163	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  ltdiv23  11959  lediv23  11960  divalglem8  16200  isdrngd  20113  deg1tm  25381  ax5seglem1  27498  ax5seglem2  27499  nvaddsub4  29220  nmoub2i  29337  cdleme21at  38589  cdleme42f  38741  trlcoabs2N  38983  tendoplcl2  39039  tendopltp  39041  cdlemk2  39093  cdlemk8  39099  cdlemk9  39100  cdlemk9bN  39101  cdleml8  39244  dihglblem3N  39556  dihglblem3aN  39557  fourierdlem42  44015  lincscm  46111  itsclc0yqsol  46450