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  8906  f1domfi2  9106  entrfi  9114  entrfir  9115  domtrfil  9116  domtrfi  9117  domtrfir  9118  php3  9133  findcard3  9183  npncan  11402  nnpcan  11404  ppncan  11423  muldivdir  11834  subdivcomb1  11836  div2neg  11864  ltmuldiv  12015  opfi1uzind  14434  sgrp2nmndlem4  18853  zndvds  21504  wsuceq123  36006  atlrelat1  39581  cvlatcvr1  39601  dih11  41525  wessf1ornlem  45429  mullimc  45862  mullimcf  45869  icccncfext  46131  stoweidlem34  46278  stoweidlem49  46293  stoweidlem57  46301  sigarexp  47103  f1ocof1ob  47327  el0ldepsnzr  48713