Theorem 3adant3l 1199

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 490	. 2 ⊢ ((𝜏 ∧ 𝜒) → 𝜒)
2		ad4ant3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	syl3an3 1183	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:  ecopovtrn  8825  rrxmet  25709  nvaddsub4  31241  adjlnop  32670  pl1cn  34569  rrnmet  38731  lflsub  40092  lflmul  40093  cvlatexch3  40363  cdleme5  41265  cdlemeg46rjgN  41547  cdlemg2l  41628  cdlemg10c  41664  tendospcanN  42048  dicvaddcl  42215  dicvscacl  42216  dochexmidlem8  42492  limsupre3lem  46686  fourierdlem42  47103  fourierdlem113  47173  ovnsupge0  47511  ovncvrrp  47518  ovnhoilem2  47556