Theorem 3adant3l 1197

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 489	. 2 ⊢ ((𝜏 ∧ 𝜒) → 𝜒)
2		ad4ant3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	syl3an3 1181	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜏 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  ecopovtrn  8806  rrxmet  25528  nvaddsub4  30918  adjlnop  32347  pl1cn  34262  rrnmet  38340  lflsub  39703  lflmul  39704  cvlatexch3  39974  cdleme5  40876  cdlemeg46rjgN  41158  cdlemg2l  41239  cdlemg10c  41275  tendospcanN  41659  dicvaddcl  41826  dicvscacl  41827  dochexmidlem8  42103  limsupre3lem  46304  fourierdlem42  46721  fourierdlem113  46791  ovnsupge0  47129  ovncvrrp  47136  ovnhoilem2  47174