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 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1103

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 1105

This theorem is referenced by:  f1dom2g  8962  f1domfi2  9162  entrfi  9170  entrfir  9171  domtrfil  9172  domtrfi  9173  domtrfir  9174  php3  9189  findcard3  9239  npncan  11474  nnpcan  11476  ppncan  11495  muldivdir  11902  subdivcomb1  11905  div2neg  11933  ltmuldiv  12083  opfi1uzind  14544  sgrp2nmndlem4  18985  zndvds  21699  wsuceq123  36304  atlrelat1  40095  cvlatcvr1  40115  dih11  42039  wessf1ornlem  45903  mullimc  46332  mullimcf  46339  icccncfext  46601  stoweidlem34  46748  stoweidlem49  46763  stoweidlem57  46771  sigarexp  47573  f1ocof1ob  47818  el0ldepsnzr  49247