Theorem 3adant3l 1182

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 1166	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜏 ∧ 𝜒)) → 𝜃)

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

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 1089

This theorem is referenced by:  ecopovtrn  8769  rrxmet  25376  nvaddsub4  30744  adjlnop  32173  pl1cn  34132  rrnmet  38074  lflsub  39437  lflmul  39438  cvlatexch3  39708  cdleme5  40610  cdlemeg46rjgN  40892  cdlemg2l  40973  cdlemg10c  41009  tendospcanN  41393  dicvaddcl  41560  dicvscacl  41561  dochexmidlem8  41837  limsupre3lem  46084  fourierdlem42  46501  fourierdlem113  46571  ovnsupge0  46909  ovncvrrp  46916  ovnhoilem2  46954