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  8916  f1domfi2  9116  entrfi  9124  entrfir  9125  domtrfil  9126  domtrfi  9127  domtrfir  9128  php3  9143  findcard3  9193  npncan  11415  nnpcan  11417  ppncan  11436  muldivdir  11847  subdivcomb1  11850  div2neg  11878  ltmuldiv  12029  opfi1uzind  14473  sgrp2nmndlem4  18899  zndvds  21529  wsuceq123  35994  atlrelat1  39767  cvlatcvr1  39787  dih11  41711  wessf1ornlem  45615  mullimc  46046  mullimcf  46053  icccncfext  46315  stoweidlem34  46462  stoweidlem49  46477  stoweidlem57  46485  sigarexp  47287  f1ocof1ob  47529  el0ldepsnzr  48943