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  8975  f1domfi2  9176  entrfi  9184  entrfir  9185  domtrfil  9186  domtrfi  9187  domtrfir  9188  php3  9203  findcard3  9253  npncan  11503  nnpcan  11505  ppncan  11524  muldivdir  11931  subdivcomb1  11934  div2neg  11962  ltmuldiv  12112  opfi1uzind  14576  sgrp2nmndlem4  19040  zndvds  21762  wsuceq123  36391  atlrelat1  40194  cvlatcvr1  40214  dih11  42138  wessf1ornlem  46017  mullimc  46446  mullimcf  46453  icccncfext  46715  stoweidlem34  46862  stoweidlem49  46877  stoweidlem57  46885  sigarexp  47687  f1ocof1ob  47969  el0ldepsnzr  49397