Theorem 3adant3l 1199

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  ecopovtrn  8844  rrxmet  25734  nvaddsub4  31264  adjlnop  32693  pl1cn  34633  rrnmet  38856  lflsub  40217  lflmul  40218  cvlatexch3  40488  cdleme5  41390  cdlemeg46rjgN  41672  cdlemg2l  41753  cdlemg10c  41789  tendospcanN  42173  dicvaddcl  42340  dicvscacl  42341  dochexmidlem8  42617  limsupre3lem  46835  fourierdlem42  47252  fourierdlem113  47322  ovnsupge0  47660  ovncvrrp  47667  ovnhoilem2  47705