Theorem syld3an1 1409

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 1136	. 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜓)
3		simp3 1137	. 2 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜃)
4		syld3an1.2	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜃) → 𝜏)
5	1, 2, 3, 4	syl3anc 1370	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 206  df-an 396  df-3an 1088

This theorem is referenced by:  f1dom2g  8969  f1domfi2  9189  entrfi  9197  entrfir  9198  domtrfil  9199  domtrfi  9200  domtrfir  9201  php3  9216  findcard3  9289  npncan  11486  nnpcan  11488  ppncan  11507  muldivdir  11912  subdivcomb1  11914  div2neg  11942  ltmuldiv  12092  opfi1uzind  14467  sgrp2nmndlem4  18846  zndvds  21325  wsuceq123  35091  atlrelat1  38495  cvlatcvr1  38515  dih11  40440  wessf1ornlem  44183  mullimc  44631  mullimcf  44638  icccncfext  44902  stoweidlem34  45049  stoweidlem49  45064  stoweidlem57  45072  sigarexp  45874  f1ocof1ob  46088  el0ldepsnzr  47236