Theorem 3adant3l 1187

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
3adant3l	⊢ ((𝜑 ∧ 𝜓 ∧ (𝜏 ∧ 𝜒)) → 𝜃)

Proof of Theorem 3adant3l

Step	Hyp	Ref	Expression
1		simpr 485	. 2 ⊢ ((𝜏 ∧ 𝜒) → 𝜒)
2		ad4ant3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	syl3an3 1171	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜏 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  ecopovtrn  8764  rrxmet  25400  nvaddsub4  30753  adjlnop  32182  pl1cn  34146  rrnmet  38203  lflsub  39566  lflmul  39567  cvlatexch3  39837  cdleme5  40739  cdlemeg46rjgN  41021  cdlemg2l  41102  cdlemg10c  41138  tendospcanN  41522  dicvaddcl  41689  dicvscacl  41690  dochexmidlem8  41966  limsupre3lem  46182  fourierdlem42  46599  fourierdlem113  46669  ovnsupge0  47007  ovncvrrp  47014  ovnhoilem2  47052