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  6834  fodomr  7461  dffi3  7680  cantnflt  7879  cantnflem1c  7894  cantnflem1  7896  cantnfltOLD  7909  cantnflem1cOLD  7917  cantnflem1OLD  7919  isfin2-2  8487  fin23lem17  8506  fin23lem39  8518  axdc3lem2  8619  ttukeylem5  8681  pwfseqlem5  8829  seqf1olem2  11845  wrdind  12370  wrd2ind  12371  rlimclim1  13022  caucvgrlem  13149  o1fsum  13275  prmind2  13773  rami  14075  ramcl  14089  poslubmo  15315  posglbmo  15316  pslem  15375  pgpfaclem2  16582  islbs3  17235  mplsubglem  17509  mpllsslem  17510  mplsubglemOLD  17511  mpllsslemOLD  17512  prmirredlem  17916  prmirredlemOLD  17919  psgndif  18031  gsummatr01lem4  18463  lmcvg  18865  lmff  18904  lmmo  18983  1stcfb  19048  1stcelcls  19064  restnlly  19085  lly1stc  19099  kgeni  19109  cnmpt12  19239  cnmpt22  19246  filss  19425  flimopn  19547  flimrest  19555  tgpt0  19688  tsmsi  19703  tsmsxp  19728  nmoleub2lem2  20670  nmoleub3  20673  cfil3i  20779  equivcfil  20809  equivcau  20810  ovolicc2lem3  21001  ovolicc2  21004  vitalilem2  21088  vitalilem3  21089  itg2seq  21219  limciun  21368  dvferm1lem  21455  dvferm2lem  21457  dvcnvrelem1  21488  dvfsumrlim  21502  dvfsum2  21505  ftc1a  21508  ftc1lem4  21510  fta1glem2  21637  plyeq0lem  21677  dgrcolem2  21740  dgrco  21741  plydivlem4  21761  fta1lem  21772  vieta1  21777  scvxcvx  22378  wilthlem2  22406  ftalem3  22411  perfectlem2  22568  2sqlem6  22707  2sqlem8  22710  dchrisumlema  22736  dchrisumlem2  22738  pthdepisspth  23472  pjoi0  25119  atomli  25785  archiabllem1a  26207  archiabllem2a  26210  sigaclcu  26559  measvun  26622  relexpindlem  27340  relexpind  27341  rtrclind  27350  ftc1cnnclem  28463  neibastop2lem  28579  sdclem2  28636  heibor1lem  28706  ismrcd1  29032  fnchoice  29749  stoweidlem20  29813  stoweidlem59  29852  telescgsum  30809  ee222  31204  ee333  31209  ee1111  31219  sbcoreleleq  31239  ordelordALT  31242  trsbc  31245  ee110  31397  ee101  31399  ee011  31401  ee100  31403  ee010  31405  ee001  31407  eel1111  31451  eel11111  31454  bnj1128  31979  bnj1204  32001  bnj1417  32030  cvrat4  33085  hdmapval2  35478
  Copyright terms: Public domain W3C validator