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  11102  lediv23  11103  divalglem8  15321  isdrngd  18970  deg1tm  24073  ax5seglem1  26003  ax5seglem2  26004  nvaddsub4  27817  nmoub2i  27934  cdleme21at  36114  cdleme42f  36266  trlcoabs2N  36508  tendoplcl2  36564  tendopltp  36566  cdlemk2  36618  cdlemk8  36624  cdlemk9  36625  cdlemk9bN  36626  cdleml8  36769  dihglblem3N  37082  dihglblem3aN  37083  fourierdlem42  40865  lincscm  42725