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

Theorem syld3an2 1231
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 1159 . . 3  |-  ( (
ph  /\  th  /\  ch )  ->  ps )
3 syld3an2.2 . . . 4  |-  ( (
ph  /\  ps  /\  th )  ->  ta )
433com23 1159 . . 3  |-  ( (
ph  /\  th  /\  ps )  ->  ta )
52, 4syld3an3 1229 . 2  |-  ( (
ph  /\  th  /\  ch )  ->  ta )
653com23 1159 1  |-  ( (
ph  /\  ch  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  nppcan2  9324  nnncan  9328  nnncan2  9330  ltdivmul  9874  ledivmul  9875  ltdiv23  9893  lediv23  9894  xrmaxlt  10761  xrltmin  10762  xrmaxle  10763  xrlemin  10764  dvdssub2  12879  dvdsgcdb  13036  vdwapun  13334  poslubdg  14567  ipodrsfi  14581  islp3  17202  bddibl  19723  gxinv  21850  gxinv2  21851  vcnegsubdi2  22046  nvpi  22147  nvabs  22154  nmmulg  24344  ghomgsg  25096  subdivcomb2  25188  lineid  26009  pell14qrgap  26929  stoweidlem22  27738  stoweidlem26  27742  sigarexp  27816  oplecon1b  29936  opltcon1b  29940  oldmm2  29953  oldmj2  29957  cmt3N  29986  2llnneN  30143  cvrexchlem  30153  pmod2iN  30583  polcon2N  30653  paddatclN  30683  osumcllem3N  30692  ltrnval1  30868  cdleme48fv  31233  cdlemg33b  31441  trlcolem  31460  cdlemh  31551  cdlemi1  31552  cdlemi2  31553  cdlemi  31554  cdlemk4  31568  cdlemk19u1  31703  cdlemn3  31932  hgmapfval  32624
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator