Theorem 3adant2r 1192

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072

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 385  df-3an 1074

This theorem is referenced by:  ltdiv23  11127  lediv23  11128  divalglem8  15346  isdrngd  18995  deg1tm  24098  ax5seglem1  26029  ax5seglem2  26030  nvaddsub4  27843  nmoub2i  27960  cdleme21at  36137  cdleme42f  36289  trlcoabs2N  36531  tendoplcl2  36587  tendopltp  36589  cdlemk2  36641  cdlemk8  36647  cdlemk9  36648  cdlemk9bN  36649  cdleml8  36792  dihglblem3N  37105  dihglblem3aN  37106  fourierdlem42  40888  lincscm  42748