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

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

Proof of Theorem syld3an3
StepHypRef Expression
1 simp1 956 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
2 simp2 957 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )
3 syld3an3.1 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
4 syld3an3.2 . 2  |-  ( (
ph  /\  ps  /\  th )  ->  ta )
51, 2, 3, 4syl3anc 1183 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 935
This theorem is referenced by:  syld3an1  1229  syld3an2  1230  brelrng  5011  resin  5601  moriotass  6476  omwordri  6712  oewordri  6732  gchaleph2  8445  gruf  8580  nnncan1  9230  lediv1  9768  lemuldiv  9782  supxrbnd  10800  bcval4  11485  ccatval3  11634  znnenlem  12698  dvdsmultr1  12771  dvdssub2  12774  ndvdsadd  12815  mrcsscl  13732  latnle  14401  latabs1  14403  latabs2  14404  latj4rot  14418  grpsubf  14755  grpinvsub  14758  grpnpcan  14767  subgsubcl  14842  divssub  14887  ghmsub  14901  odhash3  15097  dvrcl  15678  unitdvcl  15679  abvsubtri  15810  lspsntrim  16061  basgen2  16944  opnneiss  17072  restlp  17130  nmtri  18360  sincosq1lem  20083  logrec  20339  grpodivinv  21222  grpoinvdiv  21223  grpodivf  21224  gxsuc  21250  vcnegsubdi2  21444  vcsub4  21445  nvmval2  21514  nvsubadd  21526  nvaddsub4  21532  nvnncan  21534  nvpi  21545  nvmtri  21550  nvabs  21552  4ipval2  21594  ipval3  21595  isblo2  21674  blof  21676  nmblore  21677  nmlnoubi  21687  nmlnogt0  21688  shsubcl  22113  unopadj  22812  atexch  23274  atcvatlem  23278  ind1  23881  ind0  23882  inelsiga  23983  ghomf1olem  24588  btwnconn2  25467  ismtybnd  26037  mzprename  26333  pell14qrdivcl  26456  pwssplit4  26697  frlmsslss2  26751  lindsmm  26804  dvconstbi  27057  1pthon2v  27731  lkrlsp2  29364  opcon2b  29458  opltcon2b  29467  oldmm3N  29480  oldmm4  29481  oldmj3  29484  oldmj4  29485  cmt2N  29511  cmt4N  29513  atleneN  29694  lplnri2N  29814  cdlema2N  30052  pmapojoinN  30228  ltrncnvatb  30398  trlval2  30423  trljat1  30426  cdleme18c  30553  cdleme19c  30565  cdlemeiota  30845  trlcocnv  30980  tendoplco2  31039  cdlemk6  31097  cdlemk7u  31130  cdlemk22  31153  cdlemk24-3  31163  cdlemkid2  31184  cdlemk11ta  31189  cdlemk11tc  31205  cdlemk47  31209  cdlemk52  31214  tendocnv  31282  dibelval1st1  31411  dibelval1st2N  31412  dihord2pre2  31487
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 177  df-an 360  df-3an 937
  Copyright terms: Public domain W3C validator