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

Theorem syl3c 61
Description: A syllogism inference combined with contraction. (Contributed by Alan Sare, 7-Jul-2011.)
Hypotheses
Ref Expression
syl3c.1  |-  ( ph  ->  ps )
syl3c.2  |-  ( ph  ->  ch )
syl3c.3  |-  ( ph  ->  th )
syl3c.4  |-  ( ps 
->  ( ch  ->  ( th  ->  ta ) ) )
Assertion
Ref Expression
syl3c  |-  ( ph  ->  ta )

Proof of Theorem syl3c
StepHypRef Expression
1 syl3c.3 . 2  |-  ( ph  ->  th )
2 syl3c.1 . . 3  |-  ( ph  ->  ps )
3 syl3c.2 . . 3  |-  ( ph  ->  ch )
4 syl3c.4 . . 3  |-  ( ps 
->  ( ch  ->  ( th  ->  ta ) ) )
52, 3, 4sylc 60 . 2  |-  ( ph  ->  ( th  ->  ta ) )
61, 5mpd 15 1  |-  ( ph  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  tfrlem1  7044  fodomr  7667  dffi3  7890  cantnflt  8091  cantnflem1c  8106  cantnflem1  8108  cantnfltOLD  8121  cantnflem1cOLD  8129  cantnflem1OLD  8131  isfin2-2  8699  fin23lem17  8718  fin23lem39  8730  axdc3lem2  8831  ttukeylem5  8893  pwfseqlem5  9041  seqf1olem2  12123  wrdind  12678  wrd2ind  12679  rlimclim1  13344  caucvgrlem  13471  o1fsum  13603  prmind2  14102  rami  14407  ramcl  14421  poslubmo  15647  posglbmo  15648  pslem  15707  telgsums  16893  pgpfaclem2  17004  islbs3  17672  mplsubglem  17964  mpllsslem  17965  mplsubglemOLD  17966  mpllsslemOLD  17967  prmirredlem  18393  prmirredlemOLD  18396  psgndif  18508  gsummatr01lem4  19030  lmcvg  19633  lmff  19672  lmmo  19751  1stcfb  19816  1stcelcls  19832  restnlly  19853  lly1stc  19867  kgeni  19908  cnmpt12  20038  cnmpt22  20045  filss  20224  flimopn  20346  flimrest  20354  tgpt0  20487  tsmsi  20502  tsmsxp  20527  nmoleub2lem2  21469  nmoleub3  21472  cfil3i  21578  equivcfil  21608  equivcau  21609  ovolicc2lem3  21800  ovolicc2  21803  vitalilem2  21888  vitalilem3  21889  itg2seq  22019  limciun  22168  dvferm1lem  22255  dvferm2lem  22257  dvcnvrelem1  22288  dvfsumrlim  22302  dvfsum2  22305  ftc1a  22308  ftc1lem4  22310  fta1glem2  22437  plyeq0lem  22477  dgrcolem2  22540  dgrco  22541  plydivlem4  22561  fta1lem  22572  vieta1  22577  scvxcvx  23184  wilthlem2  23212  ftalem3  23217  perfectlem2  23374  2sqlem6  23513  2sqlem8  23516  dchrisumlema  23542  dchrisumlem2  23544  pthdepisspth  24445  pjoi0  26504  atomli  27170  archirng  27602  archiabllem1a  27605  archiabllem2a  27608  archiabl  27612  crefi  27720  pcmplfin  27733  sigaclcu  27987  measvun  28050  signsply0  28378  relexpindlem  28932  relexpind  28933  rtrclind  28942  ftc1cnnclem  30060  neibastop2lem  30150  sdclem2  30207  heibor1lem  30277  ismrcd1  30602  lcmneg  31182  fnchoice  31355  mullimc  31530  islptre  31533  mullimcf  31537  addlimc  31562  stoweidlem20  31691  stoweidlem59  31730  ee222  32999  ee333  33004  ee1111  33014  sbcoreleleq  33034  ordelordALT  33036  trsbc  33039  ee110  33191  ee101  33193  ee011  33195  ee100  33197  ee010  33199  ee001  33201  eel1111  33245  eel11111  33248  bnj1128  33774  bnj1204  33796  bnj1417  33825  cvrat4  34890  hdmapval2  37285
  Copyright terms: Public domain W3C validator