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  8989  f1domfi2  9190  entrfi  9198  entrfir  9199  domtrfil  9200  domtrfi  9201  domtrfir  9202  php3  9217  findcard3  9267  npncan  11572  nnpcan  11574  ppncan  11593  muldivdir  12002  subdivcomb1  12005  div2neg  12033  ltmuldiv  12183  opfi1uzind  14649  sgrp2nmndlem4  19120  zndvds  21848  wsuceq123  36556  atlrelat1  40358  cvlatcvr1  40378  dih11  42302  wessf1ornlem  46169  mullimc  46597  mullimcf  46604  icccncfext  46866  stoweidlem34  47013  stoweidlem49  47028  stoweidlem57  47036  sigarexp  47838  f1ocof1ob  48120  el0ldepsnzr  49548