Theorem syld3an1 1413

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  f1dom2g  8918  f1domfi2  9118  entrfi  9126  entrfir  9127  domtrfil  9128  domtrfi  9129  domtrfir  9130  php3  9145  findcard3  9195  npncan  11414  nnpcan  11416  ppncan  11435  muldivdir  11846  subdivcomb1  11848  div2neg  11876  ltmuldiv  12027  opfi1uzind  14446  sgrp2nmndlem4  18865  zndvds  21516  wsuceq123  36028  atlrelat1  39697  cvlatcvr1  39717  dih11  41641  wessf1ornlem  45544  mullimc  45976  mullimcf  45983  icccncfext  46245  stoweidlem34  46392  stoweidlem49  46407  stoweidlem57  46415  sigarexp  47217  f1ocof1ob  47441  el0ldepsnzr  48827