Theorem 3adant3l 1193

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  ecopovtrn  8797  rrxmet  25450  nvaddsub4  30806  adjlnop  32235  pl1cn  34213  rrnmet  38292  lflsub  39655  lflmul  39656  cvlatexch3  39926  cdleme5  40828  cdlemeg46rjgN  41110  cdlemg2l  41191  cdlemg10c  41227  tendospcanN  41611  dicvaddcl  41778  dicvscacl  41779  dochexmidlem8  42055  limsupre3lem  46270  fourierdlem42  46687  fourierdlem113  46757  ovnsupge0  47095  ovncvrrp  47102  ovnhoilem2  47140