Theorem 3adant3l 1181

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 1166	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜏 ∧ 𝜒)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 1090

This theorem is referenced by:  wfrlem12OLD  8320  ecopovtrn  8814  rrxmet  24925  nvaddsub4  29910  adjlnop  31339  pl1cn  32935  rrnmet  36697  lflsub  37937  lflmul  37938  cvlatexch3  38208  cdleme5  39111  cdlemeg46rjgN  39393  cdlemg2l  39474  cdlemg10c  39510  tendospcanN  39894  dicvaddcl  40061  dicvscacl  40062  dochexmidlem8  40338  limsupre3lem  44448  fourierdlem42  44865  fourierdlem113  44935  ovnsupge0  45273  ovncvrrp  45280  ovnhoilem2  45318