Theorem 3adant3l 1178

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 1163	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜏 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  wfrlem12OLD  8135  ecopovtrn  8583  rrxmet  24553  nvaddsub4  28998  adjlnop  30427  pl1cn  31884  rrnmet  35966  lflsub  37060  lflmul  37061  cvlatexch3  37331  cdleme5  38233  cdlemeg46rjgN  38515  cdlemg2l  38596  cdlemg10c  38632  tendospcanN  39016  dicvaddcl  39183  dicvscacl  39184  dochexmidlem8  39460  limsupre3lem  43227  fourierdlem42  43644  fourierdlem113  43714  ovnsupge0  44049  ovncvrrp  44056  ovnhoilem2  44094