Theorem syld3an1 1409

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 1136	. 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜓)
3		simp3 1137	. 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜃)
4		syld3an1.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1370	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 206  df-an 397  df-3an 1088

This theorem is referenced by:  f1dom2g  8766  f1domfi2  8977  entrfi  8985  entrfir  8986  domtrfil  8987  domtrfi  8988  domtrfir  8989  php3  9004  npncan  11251  nnpcan  11253  ppncan  11272  muldivdir  11677  subdivcomb1  11679  div2neg  11707  ltmuldiv  11857  opfi1uzind  14224  sgrp2nmndlem4  18576  zndvds  20766  wsuceq123  33817  atlrelat1  37342  cvlatcvr1  37362  dih11  39286  wessf1ornlem  42729  mullimc  43164  mullimcf  43171  icccncfext  43435  stoweidlem34  43582  stoweidlem49  43597  stoweidlem57  43605  sigarexp  44386  f1ocof1ob  44584  el0ldepsnzr  45819