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

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

This theorem is referenced by:  wfrlem12OLD  8182  ecopovtrn  8640  rrxmet  24621  nvaddsub4  29068  adjlnop  30497  pl1cn  31954  rrnmet  36035  lflsub  37281  lflmul  37282  cvlatexch3  37552  cdleme5  38454  cdlemeg46rjgN  38736  cdlemg2l  38817  cdlemg10c  38853  tendospcanN  39237  dicvaddcl  39404  dicvscacl  39405  dochexmidlem8  39681  limsupre3lem  43502  fourierdlem42  43919  fourierdlem113  43989  ovnsupge0  44325  ovncvrrp  44332  ovnhoilem2  44370