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  12033  lediv23  12034  divalglem8  16327  isdrngd  20698  isdrngdOLD  20700  deg1tm  26080  ax5seglem1  29001  ax5seglem2  29002  nvaddsub4  30732  nmoub2i  30849  cdleme21at  40584  cdleme42f  40736  trlcoabs2N  40978  tendoplcl2  41034  tendopltp  41036  cdlemk2  41088  cdlemk8  41094  cdlemk9  41095  cdlemk9bN  41096  cdleml8  41239  dihglblem3N  41551  dihglblem3aN  41552  fourierdlem42  46389  lincscm  48672  itsclc0yqsol  49006