Theorem syld3an1 1429

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 1150	. 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜓)
3		simp3 1151	. 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜃)
4		syld3an1.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1390	1 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1098

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 209  df-an 400  df-3an 1100

This theorem is referenced by:  f1dom2g  8950  f1domfi2  9150  entrfi  9158  entrfir  9159  domtrfil  9160  domtrfi  9161  domtrfir  9162  php3  9177  findcard3  9227  npncan  11452  nnpcan  11454  ppncan  11473  muldivdir  11883  subdivcomb1  11886  div2neg  11914  ltmuldiv  12065  opfi1uzind  14524  sgrp2nmndlem4  18965  zndvds  21598  wsuceq123  36159  atlrelat1  39942  cvlatcvr1  39962  dih11  41886  wessf1ornlem  45760  mullimc  46189  mullimcf  46196  icccncfext  46458  stoweidlem34  46605  stoweidlem49  46620  stoweidlem57  46628  sigarexp  47430  f1ocof1ob  47672  el0ldepsnzr  49086