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  8750  rrxmet  25336  nvaddsub4  30639  adjlnop  32068  pl1cn  33989  rrnmet  37889  lflsub  39186  lflmul  39187  cvlatexch3  39457  cdleme5  40359  cdlemeg46rjgN  40641  cdlemg2l  40722  cdlemg10c  40758  tendospcanN  41142  dicvaddcl  41309  dicvscacl  41310  dochexmidlem8  41586  limsupre3lem  45854  fourierdlem42  46271  fourierdlem113  46341  ovnsupge0  46679  ovncvrrp  46686  ovnhoilem2  46724