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

Theorem syld3an2 1311
Description: A syllogism inference. (Contributed by NM, 20-May-2007.)
Hypotheses
Ref Expression
syld3an2.1  |-  ( (
ph  /\  ch  /\  th )  ->  ps )
syld3an2.2  |-  ( (
ph  /\  ps  /\  th )  ->  ta )
Assertion
Ref Expression
syld3an2  |-  ( (
ph  /\  ch  /\  th )  ->  ta )

Proof of Theorem syld3an2
StepHypRef Expression
1 syld3an2.1 . . . 4  |-  ( (
ph  /\  ch  /\  th )  ->  ps )
213com23 1211 . . 3  |-  ( (
ph  /\  th  /\  ch )  ->  ps )
3 syld3an2.2 . . . 4  |-  ( (
ph  /\  ps  /\  th )  ->  ta )
433com23 1211 . . 3  |-  ( (
ph  /\  th  /\  ps )  ->  ta )
52, 4syld3an3 1309 . 2  |-  ( (
ph  /\  th  /\  ch )  ->  ta )
653com23 1211 1  |-  ( (
ph  /\  ch  /\  th )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 982
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  df-3an 984
This theorem is referenced by:  nppcan2  9904  nnncan  9908  nnncan2  9910  ltdivmul  10479  ledivmul  10480  ltdiv23  10497  lediv23  10498  xrmaxlt  11476  xrltmin  11477  xrmaxle  11478  xrlemin  11479  swrdtrcfv  12782  dvdssub2  14320  dvdsgcdb  14483  lcmdvdsb  14543  vdwapun  14878  poslubdg  16337  ipodrsfi  16351  matinvgcell  19382  mdetrsca2  19551  mdetrlin2  19554  mdetunilem5  19563  decpmatmul  19718  islp3  20084  bddibl  22665  gxinv  25834  gxinv2  25835  vcnegsubdi2  26030  nvpi  26131  nvabs  26138  nmmulg  28602  ghomgsg  30090  subdivcomb2  30139  lineid  30626  oplecon1b  32466  opltcon1b  32470  oldmm2  32483  oldmj2  32487  cmt3N  32516  2llnneN  32673  cvrexchlem  32683  pmod2iN  33113  polcon2N  33183  paddatclN  33213  osumcllem3N  33222  ltrnval1  33398  cdleme48fv  33765  cdlemg33b  33973  trlcolem  33992  cdlemh  34083  cdlemi1  34084  cdlemi2  34085  cdlemi  34086  cdlemk4  34100  cdlemk19u1  34235  cdlemn3  34464  hgmapfval  35156  pell14qrgap  35419  stoweidlem22  37441  stoweidlem26  37445  sigarexp  37858  pfxtrcfv  38322  pfxco  38359  lindszr  39012
  Copyright terms: Public domain W3C validator