Theorem syld3an1 1438

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  f1dom2g  9034  f1domfi2  9235  entrfi  9243  entrfir  9244  domtrfil  9245  domtrfi  9246  domtrfir  9247  php3  9262  findcard3  9312  npncan  11618  nnpcan  11620  ppncan  11639  muldivdir  12049  subdivcomb1  12052  div2neg  12080  ltmuldiv  12230  opfi1uzind  14697  sgrp2nmndlem4  19177  zndvds  21910  wsuceq123  36791  atlrelat1  40644  cvlatcvr1  40664  dih11  42588  wessf1ornlem  46473  mullimc  46901  mullimcf  46908  icccncfext  47170  stoweidlem34  47317  stoweidlem49  47332  stoweidlem57  47340  sigarexp  48142  f1ocof1ob  48424  el0ldepsnzr  49910