Theorem syld3an1 1437

Description: A syllogism inference. (Contributed by NM, 7-Jul-2008.) (Proof shortened by Wolf Lammen, 26-Jun-2022.)

Hypotheses

Ref	Expression
syld3an1.1	⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜑)
syld3an1.2	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)

Assertion

Ref	Expression
syld3an1	⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜏)

Proof of Theorem syld3an1

Step	Hyp	Ref	Expression
1		syld3an1.1	. 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜑)
2		simp2 1155	. 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜓)
3		simp3 1156	. 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜃)
4		syld3an1.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1398	1 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜏)

This proof depends on syntax axioms:   → wi 4   ∧ 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:  f1dom2g  9003  f1domfi2  9204  entrfi  9212  entrfir  9213  domtrfil  9214  domtrfi  9215  domtrfir  9216  php3  9231  findcard3  9281  npncan  11586  nnpcan  11588  ppncan  11607  muldivdir  12016  subdivcomb1  12019  div2neg  12047  ltmuldiv  12197  opfi1uzind  14663  sgrp2nmndlem4  19136  zndvds  21864  wsuceq123  36672  atlrelat1  40487  cvlatcvr1  40507  dih11  42431  wessf1ornlem  46308  mullimc  46736  mullimcf  46743  icccncfext  47005  stoweidlem34  47152  stoweidlem49  47167  stoweidlem57  47175  sigarexp  47977  f1ocof1ob  48259  el0ldepsnzr  49687