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

Theorem sylan2d 484
 Description: A syllogism deduction. (Contributed by NM, 15-Dec-2004.)
Hypotheses
Ref Expression
sylan2d.1
sylan2d.2
Assertion
Ref Expression
sylan2d

Proof of Theorem sylan2d
StepHypRef Expression
1 sylan2d.1 . . 3
2 sylan2d.2 . . . 4
32ancomsd 455 . . 3
41, 3syland 483 . 2
54ancomsd 455 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 370 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 188  df-an 372 This theorem is referenced by:  syl2and  485  sylan2i  659  swopo  4781  wfrlem5  7045  unblem1  7826  unfi  7841  prodgt02  10452  prodge02  10454  lo1mul  13679  infpnlem1  14842  ghmcnp  21116  ulmcaulem  23336  ulmcau  23337  shintcli  26968  ballotlemfc0  29321  ballotlemfcc  29322  frrlem5  30513  btwnxfr  30816  endofsegid  30845  bj-bary1lem1  31668  ltcvrntr  32908  poml4N  33437
 Copyright terms: Public domain W3C validator