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  7968  ecopovtrn  8402  rrxmet  24013  nvaddsub4  28436  adjlnop  29865  pl1cn  31200  rrnmet  35109  lflsub  36205  lflmul  36206  cvlatexch3  36476  cdleme5  37378  cdlemeg46rjgN  37660  cdlemg2l  37741  cdlemg10c  37777  tendospcanN  38161  dicvaddcl  38328  dicvscacl  38329  dochexmidlem8  38605  limsupre3lem  42020  fourierdlem42  42441  fourierdlem113  42511  ovnsupge0  42846  ovncvrrp  42853  ovnhoilem2  42891