Theorem 3adant2r 1318

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 1266	. . 3 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) → 𝜃)
3	2	3adant1r 1316	. 2 ⊢ (((𝜓 ∧ 𝜏) ∧ 𝜑 ∧ 𝜒) → 𝜃)
4	3	3com12 1266	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1036

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 197  df-an 386  df-3an 1038

This theorem is referenced by:  ltdiv23  10858  lediv23  10859  divalglem8  15047  isdrngd  18693  deg1tm  23782  ax5seglem1  25708  ax5seglem2  25709  nvaddsub4  27358  nmoub2i  27475  cdleme21at  35093  cdleme42f  35245  trlcoabs2N  35487  tendoplcl2  35543  tendopltp  35545  cdlemk2  35597  cdlemk8  35603  cdlemk9  35604  cdlemk9bN  35605  cdleml8  35748  dihglblem3N  36061  dihglblem3aN  36062  fourierdlem42  39670  lincscm  41504