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 1138	. 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜓)
3		simp3 1139	. 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜃)
4		syld3an1.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1373	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  9010  f1domfi2  9222  entrfi  9230  entrfir  9231  domtrfil  9232  domtrfi  9233  domtrfir  9234  php3  9249  findcard3  9318  npncan  11530  nnpcan  11532  ppncan  11551  muldivdir  11960  subdivcomb1  11962  div2neg  11990  ltmuldiv  12141  opfi1uzind  14550  sgrp2nmndlem4  18941  zndvds  21568  wsuceq123  35815  atlrelat1  39322  cvlatcvr1  39342  dih11  41267  wessf1ornlem  45190  mullimc  45631  mullimcf  45638  icccncfext  45902  stoweidlem34  46049  stoweidlem49  46064  stoweidlem57  46072  sigarexp  46874  f1ocof1ob  47093  el0ldepsnzr  48384