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  12189  lediv23  12190  divalglem8  16550  isdrngd  21002  isdrngdOLD  21004  deg1tm  26417  ax5seglem1  29488  ax5seglem2  29489  nvaddsub4  31241  nmoub2i  31358  eldisjs6  39840  cdleme21at  41353  cdleme42f  41505  trlcoabs2N  41747  tendoplcl2  41803  tendopltp  41805  cdlemk2  41857  cdlemk8  41863  cdlemk9  41864  cdlemk9bN  41865  cdleml8  42008  dihglblem3N  42320  dihglblem3aN  42321  fourierdlem42  47103  lincscm  49486  itsclc0yqsol  49820