Theorem syld3an1 1418

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  f1dom2g  8906  f1domfi2  9106  entrfi  9114  entrfir  9115  domtrfil  9116  domtrfi  9117  domtrfir  9118  php3  9133  findcard3  9183  npncan  11406  nnpcan  11408  ppncan  11427  muldivdir  11838  subdivcomb1  11841  div2neg  11869  ltmuldiv  12020  opfi1uzind  14464  sgrp2nmndlem4  18890  zndvds  21524  wsuceq123  36040  atlrelat1  39813  cvlatcvr1  39833  dih11  41757  wessf1ornlem  45632  mullimc  46061  mullimcf  46068  icccncfext  46330  stoweidlem34  46477  stoweidlem49  46492  stoweidlem57  46500  sigarexp  47302  f1ocof1ob  47544  el0ldepsnzr  48958