Theorem 3adant3l 1176

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  wfrlem12  7960  ecopovtrn  8394  rrxmet  24005  nvaddsub4  28428  adjlnop  29857  pl1cn  31193  rrnmet  35101  lflsub  36197  lflmul  36198  cvlatexch3  36468  cdleme5  37370  cdlemeg46rjgN  37652  cdlemg2l  37733  cdlemg10c  37769  tendospcanN  38153  dicvaddcl  38320  dicvscacl  38321  dochexmidlem8  38597  limsupre3lem  42006  fourierdlem42  42428  fourierdlem113  42498  ovnsupge0  42833  ovncvrrp  42840  ovnhoilem2  42878