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

Theorem sylan2d 482
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 454 . . 3
41, 3syland 481 . 2
54ancomsd 454 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  syl2and  483  sylan2i  655  swopo  4815  unblem1  7792  unfi  7807  prodgt02  10413  prodge02  10415  lo1mul  13450  infpnlem1  14428  ghmcnp  20613  ulmcaulem  22789  ulmcau  22790  shintcli  26247  ballotlemfc0  28431  ballotlemfcc  28432  wfrlem5  29347  frrlem5  29391  btwnxfr  29706  endofsegid  29735  bj-bary1lem1  34680  ltcvrntr  35148  poml4N  35677
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
  Copyright terms: Public domain W3C validator