Theorem syld3an1 1412

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 1373	1 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  f1dom2g  8887  f1domfi2  9086  entrfi  9094  entrfir  9095  domtrfil  9096  domtrfi  9097  domtrfir  9098  php3  9113  findcard3  9162  npncan  11377  nnpcan  11379  ppncan  11398  muldivdir  11809  subdivcomb1  11811  div2neg  11839  ltmuldiv  11990  opfi1uzind  14413  sgrp2nmndlem4  18831  zndvds  21481  wsuceq123  35848  atlrelat1  39360  cvlatcvr1  39380  dih11  41304  wessf1ornlem  45222  mullimc  45656  mullimcf  45663  icccncfext  45925  stoweidlem34  46072  stoweidlem49  46087  stoweidlem57  46095  sigarexp  46897  f1ocof1ob  47112  el0ldepsnzr  48499