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

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
StepHypRef Expression
1 syld3an1.1 . 2 ((𝜒𝜓𝜃) → 𝜑)
2 simp2 1137 . 2 ((𝜒𝜓𝜃) → 𝜓)
3 simp3 1138 . 2 ((𝜒𝜓𝜃) → 𝜃)
4 syld3an1.2 . 2 ((𝜑𝜓𝜃) → 𝜏)
51, 2, 3, 4syl3anc 1371 1 ((𝜒𝜓𝜃) → 𝜏)
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator