Theorem syld3an1 1410

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 1371	1 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜃) → 𝜏)

Syntax hints:   → wi 4   ∧ w3a 1087

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 397  df-3an 1089

This theorem is referenced by:  f1dom2g  8905  f1domfi2  9125  entrfi  9133  entrfir  9134  domtrfil  9135  domtrfi  9136  domtrfir  9137  php3  9152  findcard3  9225  npncan  11418  nnpcan  11420  ppncan  11439  muldivdir  11844  subdivcomb1  11846  div2neg  11874  ltmuldiv  12024  opfi1uzind  14392  sgrp2nmndlem4  18730  zndvds  20941  wsuceq123  34259  atlrelat1  37750  cvlatcvr1  37770  dih11  39695  wessf1ornlem  43339  mullimc  43789  mullimcf  43796  icccncfext  44060  stoweidlem34  44207  stoweidlem49  44222  stoweidlem57  44230  sigarexp  45032  f1ocof1ob  45245  el0ldepsnzr  46480