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  8892  f1domfi2  9091  entrfi  9099  entrfir  9100  domtrfil  9101  domtrfi  9102  domtrfir  9103  php3  9118  findcard3  9167  npncan  11382  nnpcan  11384  ppncan  11403  muldivdir  11814  subdivcomb1  11816  div2neg  11844  ltmuldiv  11995  opfi1uzind  14418  sgrp2nmndlem4  18836  zndvds  21486  wsuceq123  35856  atlrelat1  39419  cvlatcvr1  39439  dih11  41363  wessf1ornlem  45281  mullimc  45715  mullimcf  45722  icccncfext  45984  stoweidlem34  46131  stoweidlem49  46146  stoweidlem57  46154  sigarexp  46956  f1ocof1ob  47180  el0ldepsnzr  48567