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  8827  rrxmet  25604  nvaddsub4  31046  adjlnop  32475  pl1cn  34376  rrnmet  38521  lflsub  39882  lflmul  39883  cvlatexch3  40153  cdleme5  41055  cdlemeg46rjgN  41337  cdlemg2l  41418  cdlemg10c  41454  tendospcanN  41838  dicvaddcl  42005  dicvscacl  42006  dochexmidlem8  42282  limsupre3lem  46487  fourierdlem42  46904  fourierdlem113  46974  ovnsupge0  47312  ovncvrrp  47319  ovnhoilem2  47357