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

Theorem syld3an3 1229
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 957 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ph )
2 simp2 958 . 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 1184 1  |-  ( (
ph  /\  ps  /\  ch )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  syld3an1  1230  syld3an2  1231  brelrng  5091  resin  5689  moriotass  6571  omwordri  6807  oewordri  6827  gchaleph2  8543  gruf  8678  nnncan1  9329  lediv1  9867  lemuldiv  9881  supxrbnd  10899  bcval4  11590  ccatval3  11739  znnenlem  12803  dvdsmultr1  12876  dvdssub2  12879  ndvdsadd  12920  mrcsscl  13837  latnle  14506  latabs1  14508  latabs2  14509  latj4rot  14523  grpsubf  14860  grpinvsub  14863  grpnpcan  14872  subgsubcl  14947  divssub  14992  ghmsub  15006  odhash3  15202  dvrcl  15783  unitdvcl  15784  abvsubtri  15915  lspsntrim  16162  basgen2  17046  opnneiss  17174  restlp  17239  nmtri  18664  sincosq1lem  20397  logrec  20653  1pthon2v  21585  grpodivinv  21824  grpoinvdiv  21825  grpodivf  21826  gxsuc  21852  vcnegsubdi2  22046  vcsub4  22047  nvmval2  22116  nvsubadd  22128  nvaddsub4  22134  nvnncan  22136  nvpi  22147  nvmtri  22152  nvabs  22154  4ipval2  22196  ipval3  22197  isblo2  22276  blof  22278  nmblore  22279  nmlnoubi  22289  nmlnogt0  22290  shsubcl  22715  unopadj  23414  atexch  23876  atcvatlem  23880  ofldaddlt  24233  ind1  24408  inelsiga  24510  ghomf1olem  25097  btwnconn2  26028  ismtybnd  26497  mzprename  26787  pell14qrdivcl  26909  pwssplit4  27149  frlmsslss2  27203  lindsmm  27256  dvconstbi  27509  ibliccsinexp  27702  stoweidlem22  27728  lkrlsp2  29828  opcon2b  29922  opltcon2b  29931  oldmm3N  29944  oldmm4  29945  oldmj3  29948  oldmj4  29949  cmt2N  29975  cmt4N  29977  atleneN  30158  lplnri2N  30278  cdlema2N  30516  pmapojoinN  30692  ltrncnvatb  30862  trlval2  30887  trljat1  30890  cdleme18c  31017  cdleme19c  31029  cdlemeiota  31309  trlcocnv  31444  tendoplco2  31503  cdlemk6  31561  cdlemk7u  31594  cdlemk22  31617  cdlemk24-3  31627  cdlemkid2  31648  cdlemk11ta  31653  cdlemk11tc  31669  cdlemk47  31673  cdlemk52  31678  tendocnv  31746  dibelval1st1  31875  dibelval1st2N  31876  dihord2pre2  31951
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