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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ecopovtrn  8841  rrxmet  25729  nvaddsub4  31259  adjlnop  32688  pl1cn  34587  rrnmet  38763  lflsub  40124  lflmul  40125  cvlatexch3  40395  cdleme5  41297  cdlemeg46rjgN  41579  cdlemg2l  41660  cdlemg10c  41696  tendospcanN  42080  dicvaddcl  42247  dicvscacl  42248  dochexmidlem8  42524  limsupre3lem  46741  fourierdlem42  47158  fourierdlem113  47228  ovnsupge0  47566  ovncvrrp  47573  ovnhoilem2  47611