Theorem 3adant3l 1179

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 1164	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:  wfrlem12OLD  8359  ecopovtrn  8859  rrxmet  25456  nvaddsub4  30686  adjlnop  32115  pl1cn  33916  rrnmet  37816  lflsub  39049  lflmul  39050  cvlatexch3  39320  cdleme5  40223  cdlemeg46rjgN  40505  cdlemg2l  40586  cdlemg10c  40622  tendospcanN  41006  dicvaddcl  41173  dicvscacl  41174  dochexmidlem8  41450  limsupre3lem  45688  fourierdlem42  46105  fourierdlem113  46175  ovnsupge0  46513  ovncvrrp  46520  ovnhoilem2  46558