Theorem 3adant3l 1182

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 1166	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:  ecopovtrn  8760  rrxmet  25385  nvaddsub4  30743  adjlnop  32172  pl1cn  34115  rrnmet  38164  lflsub  39527  lflmul  39528  cvlatexch3  39798  cdleme5  40700  cdlemeg46rjgN  40982  cdlemg2l  41063  cdlemg10c  41099  tendospcanN  41483  dicvaddcl  41650  dicvscacl  41651  dochexmidlem8  41927  limsupre3lem  46178  fourierdlem42  46595  fourierdlem113  46665  ovnsupge0  47003  ovncvrrp  47010  ovnhoilem2  47048