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 207  df-an 396  df-3an 1088

This theorem is referenced by:  f1dom2g  9008  f1domfi2  9219  entrfi  9227  entrfir  9228  domtrfil  9229  domtrfi  9230  domtrfir  9231  php3  9246  findcard3  9315  npncan  11527  nnpcan  11529  ppncan  11548  muldivdir  11957  subdivcomb1  11959  div2neg  11987  ltmuldiv  12138  opfi1uzind  14546  sgrp2nmndlem4  18953  zndvds  21585  wsuceq123  35795  atlrelat1  39302  cvlatcvr1  39322  dih11  41247  wessf1ornlem  45127  mullimc  45571  mullimcf  45578  icccncfext  45842  stoweidlem34  45989  stoweidlem49  46004  stoweidlem57  46012  sigarexp  46814  f1ocof1ob  47030  el0ldepsnzr  48312