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

Theorem sylanl1 650
Description: A syllogism inference. (Contributed by NM, 10-Mar-2005.)
Hypotheses
Ref Expression
sylanl1.1
sylanl1.2
Assertion
Ref Expression
sylanl1

Proof of Theorem sylanl1
StepHypRef Expression
1 sylanl1.1 . . 3
21anim1i 568 . 2
3 sylanl1.2 . 2
42, 3sylan 471 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  adantlll  717  adantllr  718  isocnv  6226  odi  7247  oeoelem  7266  mapxpen  7703  xadddilem  11515  pcqmul  14377  infpnlem1  14428  chpdmat  19342  neitr  19681  hausflimi  20481  nmoix  21236  nmoleub  21238  metdsre  21357  pthdepisspth  24576  extwwlkfab  25090  sspph  25770  unoplin  26839  hmoplin  26861  chirredlem1  27309  mdsymlem2  27323  foresf1o  27403  ordtconlem1  27906  heicant  30049  cnambfre  30063  itg2addnclem  30066  ftc1anclem5  30094  ftc1anc  30098  rrnequiv  30331  isfldidl  30465  ispridlc  30467  reccot  33152  rectan  33153
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