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:  wfrlem12OLD  8339  ecopovtrn  8839  rrxmet  25365  nvaddsub4  30643  adjlnop  32072  pl1cn  33991  rrnmet  37858  lflsub  39090  lflmul  39091  cvlatexch3  39361  cdleme5  40264  cdlemeg46rjgN  40546  cdlemg2l  40627  cdlemg10c  40663  tendospcanN  41047  dicvaddcl  41214  dicvscacl  41215  dochexmidlem8  41491  limsupre3lem  45728  fourierdlem42  46145  fourierdlem113  46215  ovnsupge0  46553  ovncvrrp  46560  ovnhoilem2  46598