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

Theorem syld3an3 1227
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 955 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
2 simp2 956 . 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 1182 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  syld3an1  1228  syld3an2  1229  brelrng  4908  resin  5495  moriotass  6334  omwordri  6570  oewordri  6590  gchaleph2  8298  gruf  8433  nnncan1  9083  lediv1  9621  lemuldiv  9635  supxrbnd  10647  bcval4  11320  ccatval3  11433  znnenlem  12490  dvdsmultr1  12563  dvdssub2  12566  ndvdsadd  12607  mrcsscl  13522  latnle  14191  latabs1  14193  latabs2  14194  latj4rot  14208  grpsubf  14545  grpinvsub  14548  grpnpcan  14557  subgsubcl  14632  divssub  14677  ghmsub  14691  odhash3  14887  dvrcl  15468  unitdvcl  15469  abvsubtri  15600  lspsntrim  15851  basgen2  16727  opnneiss  16855  restlp  16913  nmtri  18147  sincosq1lem  19865  logrec  20117  grpodivinv  20911  grpoinvdiv  20912  grpodivf  20913  gxsuc  20939  vcnegsubdi2  21131  vcsub4  21132  nvmval2  21201  nvsubadd  21213  nvaddsub4  21219  nvnncan  21221  nvpi  21232  nvmtri  21237  nvabs  21239  4ipval2  21281  ipval3  21282  isblo2  21361  blof  21363  nmblore  21364  nmlnoubi  21374  nmlnogt0  21375  shsubcl  21800  unopadj  22499  atexch  22961  atcvatlem  22965  inelsiga  23496  ind1  23602  ind0  23603  ghomf1olem  24001  btwnconn2  24725  grpodivzer  25377  multinvb  25423  mult2inv  25424  clsint  25513  dmse2  25604  2wsms  25608  flfneicn  25625  mulmulvec  25687  distmlva  25688  isntr  25873  islimcat  25876  fnctartar3  25909  ismtybnd  26531  mzprename  26827  pell14qrdivcl  26950  pwssplit4  27191  frlmsslss2  27245  lindsmm  27298  dvconstbi  27551  lkrlsp2  29293  opcon2b  29387  opltcon2b  29396  oldmm3N  29409  oldmm4  29410  oldmj3  29413  oldmj4  29414  cmt2N  29440  cmt4N  29442  atleneN  29623  lplnri2N  29743  cdlema2N  29981  pmapojoinN  30157  ltrncnvatb  30327  trlval2  30352  trljat1  30355  cdleme18c  30482  cdleme19c  30494  cdlemeiota  30774  trlcocnv  30909  tendoplco2  30968  cdlemk6  31026  cdlemk7u  31059  cdlemk22  31082  cdlemk24-3  31092  cdlemkid2  31113  cdlemk11ta  31118  cdlemk11tc  31134  cdlemk47  31138  cdlemk52  31143  tendocnv  31211  dibelval1st1  31340  dibelval1st2N  31341  dihord2pre2  31416
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 936
  Copyright terms: Public domain W3C validator