Theorem 3adant3l 1180

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 397  df-3an 1089

This theorem is referenced by:  wfrlem12OLD  8322  ecopovtrn  8816  rrxmet  24932  nvaddsub4  29948  adjlnop  31377  pl1cn  33004  rrnmet  36783  lflsub  38023  lflmul  38024  cvlatexch3  38294  cdleme5  39197  cdlemeg46rjgN  39479  cdlemg2l  39560  cdlemg10c  39596  tendospcanN  39980  dicvaddcl  40147  dicvscacl  40148  dochexmidlem8  40424  limsupre3lem  44527  fourierdlem42  44944  fourierdlem113  45014  ovnsupge0  45352  ovncvrrp  45359  ovnhoilem2  45397