Theorem syld3an1 1413

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 1138	. 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜓)
3		simp3 1139	. 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜃)
4		syld3an1.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1374	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 207  df-an 396  df-3an 1089

This theorem is referenced by:  f1dom2g  8910  f1domfi2  9110  entrfi  9118  entrfir  9119  domtrfil  9120  domtrfi  9121  domtrfir  9122  php3  9137  findcard3  9187  npncan  11409  nnpcan  11411  ppncan  11430  muldivdir  11841  subdivcomb1  11844  div2neg  11872  ltmuldiv  12023  opfi1uzind  14467  sgrp2nmndlem4  18893  zndvds  21542  wsuceq123  36013  atlrelat1  39784  cvlatcvr1  39804  dih11  41728  wessf1ornlem  45636  mullimc  46067  mullimcf  46074  icccncfext  46336  stoweidlem34  46483  stoweidlem49  46498  stoweidlem57  46506  sigarexp  47308  f1ocof1ob  47544  el0ldepsnzr  48958