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  8754  rrxmet  25324  nvaddsub4  30619  adjlnop  32048  pl1cn  33921  rrnmet  37808  lflsub  39045  lflmul  39046  cvlatexch3  39316  cdleme5  40219  cdlemeg46rjgN  40501  cdlemg2l  40582  cdlemg10c  40618  tendospcanN  41002  dicvaddcl  41169  dicvscacl  41170  dochexmidlem8  41446  limsupre3lem  45714  fourierdlem42  46131  fourierdlem113  46201  ovnsupge0  46539  ovncvrrp  46546  ovnhoilem2  46584