Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  syld3an1 Structured version   Visualization version   GIF version

Theorem syld3an1 1516
 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
StepHypRef Expression
1 syld3an1.1 . 2 ((𝜒𝜓𝜃) → 𝜑)
2 simp2 1131 . 2 ((𝜒𝜓𝜃) → 𝜓)
3 simp3 1132 . 2 ((𝜒𝜓𝜃) → 𝜃)
4 syld3an1.2 . 2 ((𝜑𝜓𝜃) → 𝜏)
51, 2, 3, 4syl3anc 1476 1 ((𝜒𝜓𝜃) → 𝜏)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ w3a 1071 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 197  df-an 383  df-3an 1073 This theorem is referenced by:  npncan  10504  nnpcan  10506  ppncan  10525  muldivdir  10922  div2neg  10950  ltmuldiv  11098  opfi1uzind  13485  sgrp2nmndlem4  17623  zndvds  20113  subdivcomb1  31949  wsuceq123  32096  atlrelat1  35130  cvlatcvr1  35150  dih11  37075  mullimc  40366  mullimcf  40373  icccncfext  40618  stoweidlem34  40768  stoweidlem49  40783  stoweidlem57  40791  sigarexp  41568  el0ldepsnzr  42784
 Copyright terms: Public domain W3C validator