Theorem 3adant3l 1181

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  ecopovtrn  8757  rrxmet  25364  nvaddsub4  30732  adjlnop  32161  pl1cn  34112  rrnmet  38026  lflsub  39323  lflmul  39324  cvlatexch3  39594  cdleme5  40496  cdlemeg46rjgN  40778  cdlemg2l  40859  cdlemg10c  40895  tendospcanN  41279  dicvaddcl  41446  dicvscacl  41447  dochexmidlem8  41723  limsupre3lem  45972  fourierdlem42  46389  fourierdlem113  46459  ovnsupge0  46797  ovncvrrp  46804  ovnhoilem2  46842