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  8872  rrxmet  25762  nvaddsub4  31292  adjlnop  32721  pl1cn  34670  rrnmet  38966  lflsub  40327  lflmul  40328  cvlatexch3  40598  cdleme5  41500  cdlemeg46rjgN  41782  cdlemg2l  41863  cdlemg10c  41899  tendospcanN  42283  dicvaddcl  42450  dicvscacl  42451  dochexmidlem8  42727  limsupre3lem  46957  fourierdlem42  47374  fourierdlem113  47444  ovnsupge0  47782  ovncvrrp  47789  ovnhoilem2  47827