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

Theorem syld3an1 1265
Description: A syllogism inference. (Contributed by NM, 7-Jul-2008.)
Hypotheses
Ref Expression
syld3an1.1
syld3an1.2
Assertion
Ref Expression
syld3an1

Proof of Theorem syld3an1
StepHypRef Expression
1 syld3an1.1 . . . 4
213com13 1193 . . 3
3 syld3an1.2 . . . 4
433com13 1193 . . 3
52, 4syld3an3 1264 . 2
653com13 1193 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\w3a 965
This theorem is referenced by:  npncan  9767  nnpcan  9769  ppncan  9788  div2neg  10191  ltmuldiv  10339  zndvds  18175  subdivcomb1  27840  stoweidlem34  30563  stoweidlem49  30578  stoweidlem57  30586  sigarexp  30772  el0ldepsnzr  31773  atlrelat1  33817  cvlatcvr1  33837  dih11  35761
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 185  df-an 371  df-3an 967
  Copyright terms: Public domain W3C validator