Theorem 3adant3l 1199

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 489	. 2 ⊢ ((𝜏 ∧ 𝜒) → 𝜒)
2		ad4ant3.1	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	1, 2	syl3an3 1183	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜏 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  ecopovtrn  8819  rrxmet  25548  nvaddsub4  30987  adjlnop  32416  pl1cn  34323  rrnmet  38458  lflsub  39819  lflmul  39820  cvlatexch3  40090  cdleme5  40992  cdlemeg46rjgN  41274  cdlemg2l  41355  cdlemg10c  41391  tendospcanN  41775  dicvaddcl  41942  dicvscacl  41943  dochexmidlem8  42219  limsupre3lem  46426  fourierdlem42  46843  fourierdlem113  46913  ovnsupge0  47251  ovncvrrp  47258  ovnhoilem2  47296