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  8918  f1domfi2  9123  entrfi  9131  entrfir  9132  domtrfil  9133  domtrfi  9134  domtrfir  9135  php3  9150  findcard3  9205  npncan  11419  nnpcan  11421  ppncan  11440  muldivdir  11851  subdivcomb1  11853  div2neg  11881  ltmuldiv  12032  opfi1uzind  14452  sgrp2nmndlem4  18831  zndvds  21435  wsuceq123  35775  atlrelat1  39287  cvlatcvr1  39307  dih11  41232  wessf1ornlem  45152  mullimc  45587  mullimcf  45594  icccncfext  45858  stoweidlem34  46005  stoweidlem49  46020  stoweidlem57  46028  sigarexp  46830  f1ocof1ob  47055  el0ldepsnzr  48429