Theorem 3adant2r 1198

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ltdiv23  12124  lediv23  12125  divalglem8  16483  isdrngd  20905  isdrngdOLD  20907  deg1tm  26313  ax5seglem1  29315  ax5seglem2  29316  nvaddsub4  31046  nmoub2i  31163  eldisjs6  39630  cdleme21at  41143  cdleme42f  41295  trlcoabs2N  41537  tendoplcl2  41593  tendopltp  41595  cdlemk2  41647  cdlemk8  41653  cdlemk9  41654  cdlemk9bN  41655  cdleml8  41798  dihglblem3N  42110  dihglblem3aN  42111  fourierdlem42  46904  lincscm  49251  itsclc0yqsol  49585