Theorem syld3an1 1435

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  f1dom2g  8965  f1domfi2  9165  entrfi  9173  entrfir  9174  domtrfil  9175  domtrfi  9176  domtrfir  9177  php3  9192  findcard3  9242  npncan  11478  nnpcan  11480  ppncan  11499  muldivdir  11906  subdivcomb1  11909  div2neg  11937  ltmuldiv  12087  opfi1uzind  14547  sgrp2nmndlem4  18989  zndvds  21667  wsuceq123  36202  atlrelat1  39984  cvlatcvr1  40004  dih11  41928  wessf1ornlem  45794  mullimc  46223  mullimcf  46230  icccncfext  46492  stoweidlem34  46639  stoweidlem49  46654  stoweidlem57  46662  sigarexp  47464  f1ocof1ob  47706  el0ldepsnzr  49131