Theorem 3adant2r 1176

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  ltdiv23  12157  lediv23  12158  divalglem8  16402  isdrngd  20743  isdrngdOLD  20745  deg1tm  26146  ax5seglem1  28862  ax5seglem2  28863  nvaddsub4  30590  nmoub2i  30707  cdleme21at  40027  cdleme42f  40179  trlcoabs2N  40421  tendoplcl2  40477  tendopltp  40479  cdlemk2  40531  cdlemk8  40537  cdlemk9  40538  cdlemk9bN  40539  cdleml8  40682  dihglblem3N  40994  dihglblem3aN  40995  fourierdlem42  45770  lincscm  47813  itsclc0yqsol  48152