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

Theorem syld3an1 1274
 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 1201 . . 3
3 syld3an1.2 . . . 4
433com13 1201 . . 3
52, 4syld3an3 1273 . 2
653com13 1201 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   w3a 973 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  df-3an 975 This theorem is referenced by:  npncan  9859  nnpcan  9861  ppncan  9880  div2neg  10288  ltmuldiv  10436  sgrp2nmndlem4  16173  zndvds  18715  subdivcomb1  29323  wsuceq123  29587  mullimc  31825  mullimcf  31832  icccncfext  31893  stoweidlem34  32019  stoweidlem49  32034  stoweidlem57  32042  sigarexp  32279  el0ldepsnzr  33212  atlrelat1  35189  cvlatcvr1  35209  dih11  37135
 Copyright terms: Public domain W3C validator