Theorem syld3an1 1410

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  f1dom2g  9029  f1domfi2  9248  entrfi  9256  entrfir  9257  domtrfil  9258  domtrfi  9259  domtrfir  9260  php3  9275  findcard3  9346  npncan  11557  nnpcan  11559  ppncan  11578  muldivdir  11987  subdivcomb1  11989  div2neg  12017  ltmuldiv  12168  opfi1uzind  14560  sgrp2nmndlem4  18963  zndvds  21591  wsuceq123  35778  atlrelat1  39277  cvlatcvr1  39297  dih11  41222  wessf1ornlem  45092  mullimc  45537  mullimcf  45544  icccncfext  45808  stoweidlem34  45955  stoweidlem49  45970  stoweidlem57  45978  sigarexp  46780  f1ocof1ob  46996  el0ldepsnzr  48196