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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  wfrlem12OLD  8376  ecopovtrn  8878  rrxmet  25461  nvaddsub4  30689  adjlnop  32118  pl1cn  33901  rrnmet  37789  lflsub  39023  lflmul  39024  cvlatexch3  39294  cdleme5  40197  cdlemeg46rjgN  40479  cdlemg2l  40560  cdlemg10c  40596  tendospcanN  40980  dicvaddcl  41147  dicvscacl  41148  dochexmidlem8  41424  limsupre3lem  45653  fourierdlem42  46070  fourierdlem113  46140  ovnsupge0  46478  ovncvrrp  46485  ovnhoilem2  46523