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  8767  rrxmet  25375  nvaddsub4  30728  adjlnop  32157  pl1cn  34099  rrnmet  38150  lflsub  39513  lflmul  39514  cvlatexch3  39784  cdleme5  40686  cdlemeg46rjgN  40968  cdlemg2l  41049  cdlemg10c  41085  tendospcanN  41469  dicvaddcl  41636  dicvscacl  41637  dochexmidlem8  41913  limsupre3lem  46160  fourierdlem42  46577  fourierdlem113  46647  ovnsupge0  46985  ovncvrrp  46992  ovnhoilem2  47030