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  12020  lediv23  12021  divalglem8  16313  isdrngd  20682  isdrngdOLD  20684  deg1tm  26052  ax5seglem1  28908  ax5seglem2  28909  nvaddsub4  30639  nmoub2i  30756  cdleme21at  40448  cdleme42f  40600  trlcoabs2N  40842  tendoplcl2  40898  tendopltp  40900  cdlemk2  40952  cdlemk8  40958  cdlemk9  40959  cdlemk9bN  40960  cdleml8  41103  dihglblem3N  41415  dihglblem3aN  41416  fourierdlem42  46272  lincscm  48556  itsclc0yqsol  48890