MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syld3an3 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  5066  resin  5664  moriotass  6546  omwordri  6782  oewordri  6802  gchaleph2  8515  gruf  8650  nnncan1  9301  lediv1  9839  lemuldiv  9853  supxrbnd  10871  bcval4  11561  ccatval3  11710  znnenlem  12774  dvdsmultr1  12847  dvdssub2  12850  ndvdsadd  12891  mrcsscl  13808  latnle  14477  latabs1  14479  latabs2  14480  latj4rot  14494  grpsubf  14831  grpinvsub  14834  grpnpcan  14843  subgsubcl  14918  divssub  14963  ghmsub  14977  odhash3  15173  dvrcl  15754  unitdvcl  15755  abvsubtri  15886  lspsntrim  16133  basgen2  17017  opnneiss  17145  restlp  17209  nmtri  18633  sincosq1lem  20366  logrec  20622  1pthon2v  21554  grpodivinv  21793  grpoinvdiv  21794  grpodivf  21795  gxsuc  21821  vcnegsubdi2  22015  vcsub4  22016  nvmval2  22085  nvsubadd  22097  nvaddsub4  22103  nvnncan  22105  nvpi  22116  nvmtri  22121  nvabs  22123  4ipval2  22165  ipval3  22166  isblo2  22245  blof  22247  nmblore  22248  nmlnoubi  22258  nmlnogt0  22259  shsubcl  22684  unopadj  23383  atexch  23845  atcvatlem  23849  ofldaddlt  24202  ind1  24377  inelsiga  24479  ghomf1olem  25066  btwnconn2  25948  ismtybnd  26414  mzprename  26704  pell14qrdivcl  26826  pwssplit4  27067  frlmsslss2  27121  lindsmm  27174  dvconstbi  27427  ibliccsinexp  27620  stoweidlem22  27646  lkrlsp2  29598  opcon2b  29692  opltcon2b  29701  oldmm3N  29714  oldmm4  29715  oldmj3  29718  oldmj4  29719  cmt2N  29745  cmt4N  29747  atleneN  29928  lplnri2N  30048  cdlema2N  30286  pmapojoinN  30462  ltrncnvatb  30632  trlval2  30657  trljat1  30660  cdleme18c  30787  cdleme19c  30799  cdlemeiota  31079  trlcocnv  31214  tendoplco2  31273  cdlemk6  31331  cdlemk7u  31364  cdlemk22  31387  cdlemk24-3  31397  cdlemkid2  31418  cdlemk11ta  31423  cdlemk11tc  31439  cdlemk47  31443  cdlemk52  31448  tendocnv  31516  dibelval1st1  31645  dibelval1st2N  31646  dihord2pre2  31721
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