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

Theorem sylanl2 651
 Description: A syllogism inference. (Contributed by NM, 1-Jan-2005.)
Hypotheses
Ref Expression
sylanl2.1
sylanl2.2
Assertion
Ref Expression
sylanl2

Proof of Theorem sylanl2
StepHypRef Expression
1 sylanl2.1 . . 3
21anim2i 569 . 2
3 sylanl2.2 . 2
42, 3sylan 471 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\wa 369 This theorem is referenced by:  mpanlr1  686  adantlrl  719  adantlrr  720  oesuclem  7194  oelim  7203  mulsub  10024  divsubdiv  10285  vdwlem12  14510  dpjidcl  17107  dpjidclOLD  17114  mplbas2  18134  monmat2matmon  19325  bwth  19910  cnextfun  20564  elbl4  21079  metucnOLD  21091  metucn  21092  dvradcnv  22816  dchrisum0lem2a  23702  axcontlem4  24270  cnlnadjlem2  26987  chirredlem2  27310  mdsymlem5  27326  sibfof  28282  unichnidl  30428  dmncan2  30474  jm2.26  30944  radcnvrat  31195  lcmneg  31209  binomcxplemnotnn0  31261  dvnmptdivc  31735  fourierdlem64  31953  fourierdlem74  31963  fourierdlem75  31964  fourierdlem83  31972  etransclem35  32052  cvrexchlem  35143 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