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  8941  f1domfi2  9146  entrfi  9154  entrfir  9155  domtrfil  9156  domtrfi  9157  domtrfir  9158  php3  9173  findcard3  9229  npncan  11443  nnpcan  11445  ppncan  11464  muldivdir  11875  subdivcomb1  11877  div2neg  11905  ltmuldiv  12056  opfi1uzind  14476  sgrp2nmndlem4  18855  zndvds  21459  wsuceq123  35802  atlrelat1  39314  cvlatcvr1  39334  dih11  41259  wessf1ornlem  45179  mullimc  45614  mullimcf  45621  icccncfext  45885  stoweidlem34  46032  stoweidlem49  46047  stoweidlem57  46055  sigarexp  46857  f1ocof1ob  47082  el0ldepsnzr  48456