MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syld3an2 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  9265  nnncan  9269  nnncan2  9271  ltdivmul  9815  ledivmul  9816  ltdiv23  9834  lediv23  9835  xrmaxlt  10702  xrltmin  10703  xrmaxle  10704  xrlemin  10705  dvdssub2  12815  dvdsgcdb  12972  vdwapun  13270  poslubdg  14503  ipodrsfi  14517  bddibl  19599  gxinv  21707  gxinv2  21708  vcnegsubdi2  21903  nvpi  22004  nvabs  22011  nmmulg  24154  ghomgsg  24884  subdivcomb2  24976  lineid  25732  pell14qrgap  26630  stoweidlem22  27440  stoweidlem26  27444  sigarexp  27518  oplecon1b  29317  opltcon1b  29321  oldmm2  29334  oldmj2  29338  cmt3N  29367  2llnneN  29524  cvrexchlem  29534  pmod2iN  29964  polcon2N  30034  paddatclN  30064  osumcllem3N  30073  ltrnval1  30249  cdleme48fv  30614  cdlemg33b  30822  trlcolem  30841  cdlemh  30932  cdlemi1  30933  cdlemi2  30934  cdlemi  30935  cdlemk4  30949  cdlemk19u1  31084  cdlemn3  31313  hgmapfval  32005
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