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  8982  f1domfi2  9194  entrfi  9202  entrfir  9203  domtrfil  9204  domtrfi  9205  domtrfir  9206  php3  9221  findcard3  9288  npncan  11502  nnpcan  11504  ppncan  11523  muldivdir  11932  subdivcomb1  11934  div2neg  11962  ltmuldiv  12113  opfi1uzind  14527  sgrp2nmndlem4  18904  zndvds  21508  wsuceq123  35778  atlrelat1  39285  cvlatcvr1  39305  dih11  41230  wessf1ornlem  45157  mullimc  45593  mullimcf  45600  icccncfext  45864  stoweidlem34  46011  stoweidlem49  46026  stoweidlem57  46034  sigarexp  46836  f1ocof1ob  47058  el0ldepsnzr  48391