Theorem syld3an1 1437

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  f1dom2g  8972  f1domfi2  9173  entrfi  9181  entrfir  9182  domtrfil  9183  domtrfi  9184  domtrfir  9185  php3  9200  findcard3  9250  npncan  11494  nnpcan  11496  ppncan  11515  muldivdir  11922  subdivcomb1  11925  div2neg  11953  ltmuldiv  12103  opfi1uzind  14566  sgrp2nmndlem4  19027  zndvds  21749  wsuceq123  36341  atlrelat1  40153  cvlatcvr1  40173  dih11  42097  wessf1ornlem  45961  mullimc  46390  mullimcf  46397  icccncfext  46659  stoweidlem34  46806  stoweidlem49  46821  stoweidlem57  46829  sigarexp  47631  f1ocof1ob  47876  el0ldepsnzr  49304