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  12013  lediv23  12014  divalglem8  16311  isdrngd  20681  isdrngdOLD  20683  deg1tm  26052  ax5seglem1  28907  ax5seglem2  28908  nvaddsub4  30635  nmoub2i  30752  cdleme21at  40373  cdleme42f  40525  trlcoabs2N  40767  tendoplcl2  40823  tendopltp  40825  cdlemk2  40877  cdlemk8  40883  cdlemk9  40884  cdlemk9bN  40885  cdleml8  41028  dihglblem3N  41340  dihglblem3aN  41341  fourierdlem42  46193  lincscm  48468  itsclc0yqsol  48802