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  8902  f1domfi2  9106  entrfi  9114  entrfir  9115  domtrfil  9116  domtrfi  9117  domtrfir  9118  php3  9133  findcard3  9187  npncan  11404  nnpcan  11406  ppncan  11425  muldivdir  11836  subdivcomb1  11838  div2neg  11866  ltmuldiv  12017  opfi1uzind  14437  sgrp2nmndlem4  18821  zndvds  21475  wsuceq123  35807  atlrelat1  39319  cvlatcvr1  39339  dih11  41264  wessf1ornlem  45183  mullimc  45617  mullimcf  45624  icccncfext  45888  stoweidlem34  46035  stoweidlem49  46050  stoweidlem57  46058  sigarexp  46860  f1ocof1ob  47085  el0ldepsnzr  48472