Theorem syld3an1 1410

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 1371	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 206  df-an 397  df-3an 1089

This theorem is referenced by:  f1dom2g  8916  f1domfi2  9136  entrfi  9144  entrfir  9145  domtrfil  9146  domtrfi  9147  domtrfir  9148  php3  9163  findcard3  9236  npncan  11431  nnpcan  11433  ppncan  11452  muldivdir  11857  subdivcomb1  11859  div2neg  11887  ltmuldiv  12037  opfi1uzind  14412  sgrp2nmndlem4  18752  zndvds  20993  wsuceq123  34475  atlrelat1  37856  cvlatcvr1  37876  dih11  39801  wessf1ornlem  43525  mullimc  43977  mullimcf  43984  icccncfext  44248  stoweidlem34  44395  stoweidlem49  44410  stoweidlem57  44418  sigarexp  45220  f1ocof1ob  45433  el0ldepsnzr  46668