Theorem syld3an1 1408

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 1135	. 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜓)
3		simp3 1136	. 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜃)
4		syld3an1.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1369	1 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 395  df-3an 1087

This theorem is referenced by:  f1dom2g  8967  f1domfi2  9187  entrfi  9195  entrfir  9196  domtrfil  9197  domtrfi  9198  domtrfir  9199  php3  9214  findcard3  9287  npncan  11485  nnpcan  11487  ppncan  11506  muldivdir  11911  subdivcomb1  11913  div2neg  11941  ltmuldiv  12091  opfi1uzind  14466  sgrp2nmndlem4  18845  zndvds  21324  wsuceq123  35090  atlrelat1  38494  cvlatcvr1  38514  dih11  40439  wessf1ornlem  44182  mullimc  44630  mullimcf  44637  icccncfext  44901  stoweidlem34  45048  stoweidlem49  45063  stoweidlem57  45071  sigarexp  45873  f1ocof1ob  46087  el0ldepsnzr  47235