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

Theorem syld3an2 1276
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 1203 . . 3  |-  ( (
ph  /\  th  /\  ch )  ->  ps )
3 syld3an2.2 . . . 4  |-  ( (
ph  /\  ps  /\  th )  ->  ta )
433com23 1203 . . 3  |-  ( (
ph  /\  th  /\  ps )  ->  ta )
52, 4syld3an3 1274 . 2  |-  ( (
ph  /\  th  /\  ch )  ->  ta )
653com23 1203 1  |-  ( (
ph  /\  ch  /\  th )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 974
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 976
This theorem is referenced by:  nppcan2  9855  nnncan  9859  nnncan2  9861  ltdivmul  10424  ledivmul  10425  ltdiv23  10443  lediv23  10444  xrmaxlt  11393  xrltmin  11394  xrmaxle  11395  xrlemin  11396  swrdtrcfv  12650  dvdssub2  14005  dvdsgcdb  14164  vdwapun  14474  poslubdg  15758  ipodrsfi  15772  matinvgcell  18915  mdetrsca2  19084  mdetrlin2  19087  mdetunilem5  19096  decpmatmul  19251  islp3  19625  bddibl  22224  gxinv  25250  gxinv2  25251  vcnegsubdi2  25446  nvpi  25547  nvabs  25554  nmmulg  27927  ghomgsg  29011  subdivcomb2  29084  lineid  29709  pell14qrgap  30787  lcmdvdsb  31193  stoweidlem22  31758  stoweidlem26  31762  sigarexp  32030  lindszr  32940  oplecon1b  34801  opltcon1b  34805  oldmm2  34818  oldmj2  34822  cmt3N  34851  2llnneN  35008  cvrexchlem  35018  pmod2iN  35448  polcon2N  35518  paddatclN  35548  osumcllem3N  35557  ltrnval1  35733  cdleme48fv  36100  cdlemg33b  36308  trlcolem  36327  cdlemh  36418  cdlemi1  36419  cdlemi2  36420  cdlemi  36421  cdlemk4  36435  cdlemk19u1  36570  cdlemn3  36799  hgmapfval  37491
  Copyright terms: Public domain W3C validator