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

Theorem syld3an1 1249
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 1177 . . 3
3 syld3an1.2 . . . 4
433com13 1177 . . 3
52, 4syld3an3 1248 . 2
653com13 1177 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\w3a 950
This theorem is referenced by:  npncan  9576  nnpcan  9578  ppncan  9597  div2neg  10000  ltmuldiv  10148  zndvds  17690  subdivcomb1  27086  stoweidlem34  29503  stoweidlem49  29518  stoweidlem57  29526  sigarexp  29569  el0ldepsnzr  30585  atlrelat1  32403  cvlatcvr1  32423  dih11  34347
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 179  df-an 364  df-3an 952
  Copyright terms: Public domain W3C validator