Theorem 3adant2r 1313

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)

Hypothesis

Ref	Expression
3adant1l.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3adant2r	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Proof of Theorem 3adant2r

Step	Hyp	Ref	Expression
1		3adant1l.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3com12 1261	. . 3 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)
3	2	3adant1r 1311	. 2 ⊢ (((𝜓 ∧ 𝜏) ∧ 𝜑 ∧ 𝜒) → 𝜃)
4	3	3com12 1261	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  ltdiv23  10793  lediv23  10794  divalglem8  14961  isdrngd  18595  deg1tm  23682  ax5seglem1  25608  ax5seglem2  25609  nvaddsub4  26896  nmoub2i  27013  cdleme21at  34634  cdleme42f  34786  trlcoabs2N  35028  tendoplcl2  35084  tendopltp  35086  cdlemk2  35138  cdlemk8  35144  cdlemk9  35145  cdlemk9bN  35146  cdleml8  35289  dihglblem3N  35602  dihglblem3aN  35603  fourierdlem42  39042  lincscm  42013