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  9102  entrfi  9110  entrfir  9111  domtrfil  9112  domtrfi  9113  domtrfir  9114  php3  9129  findcard3  9178  npncan  11393  nnpcan  11395  ppncan  11414  muldivdir  11825  subdivcomb1  11827  div2neg  11855  ltmuldiv  12006  opfi1uzind  14425  sgrp2nmndlem4  18844  zndvds  21495  wsuceq123  35928  atlrelat1  39493  cvlatcvr1  39513  dih11  41437  wessf1ornlem  45345  mullimc  45778  mullimcf  45785  icccncfext  46047  stoweidlem34  46194  stoweidlem49  46209  stoweidlem57  46217  sigarexp  47019  f1ocof1ob  47243  el0ldepsnzr  48629