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

Theorem syl3c 63
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 62 . 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  7093  fodomr  7720  dffi3  7942  cantnflt  8167  cantnflem1c  8182  cantnflem1  8184  isfin2-2  8738  fin23lem17  8757  fin23lem39  8769  axdc3lem2  8870  ttukeylem5  8932  pwfseqlem5  9077  seqf1olem2  12239  wrdind  12807  wrd2ind  12808  relexpindlem  13094  rtrclind  13096  rlimclim1  13576  caucvgrlem  13703  caucvgrlemOLD  13704  o1fsum  13840  lcmneg  14528  prmind2  14595  rami  14932  ramcl  14947  poslubmo  16344  posglbmo  16345  pslem  16404  telgsums  17564  pgpfaclem2  17656  islbs3  18319  mplsubglem  18599  mpllsslem  18600  prmirredlem  19001  psgndif  19107  gsummatr01lem4  19620  lmcvg  20215  lmff  20254  lmmo  20333  1stcfb  20397  1stcelcls  20413  restnlly  20434  lly1stc  20448  kgeni  20489  cnmpt12  20619  cnmpt22  20626  filss  20805  flimopn  20927  flimrest  20935  tgpt0  21070  tsmsi  21085  tsmsxp  21106  nmoleub2lem2  22049  nmoleub3  22052  cfil3i  22158  equivcfil  22188  equivcau  22189  ovolicc2lem3  22379  ovolicc2  22383  vitalilem2  22474  vitalilem3  22475  itg2seq  22607  limciun  22756  dvferm1lem  22843  dvferm2lem  22845  dvcnvrelem1  22876  dvfsumrlim  22890  dvfsum2  22893  ftc1a  22896  ftc1lem4  22898  fta1glem2  23024  plyeq0lem  23071  dgrcolem2  23135  dgrco  23136  plydivlem4  23156  fta1lem  23167  vieta1  23172  scvxcvx  23815  wilthlem2  23898  ftalem3  23903  perfectlem2  24060  2sqlem6  24199  2sqlem8  24202  dchrisumlema  24228  dchrisumlem2  24230  pthdepisspth  25190  pjoi0  27246  atomli  27911  archirng  28384  archiabllem1a  28387  archiabllem2a  28390  archiabl  28394  crefi  28554  pcmplfin  28567  sigaclcu  28819  measvun  28911  signsply0  29269  bnj1128  29628  bnj1204  29650  bnj1417  29679  neibastop2lem  30842  poimirlem31  31719  ftc1cnnclem  31763  sdclem2  31819  heibor1lem  31889  cvrat4  32761  hdmapval2  35156  ismrcd1  35293  relexpxpmin  35996  ee222  36543  ee333  36548  ee1111  36558  sbcoreleleq  36581  ordelordALT  36583  trsbc  36586  ee110  36742  ee101  36744  ee011  36746  ee100  36748  ee010  36750  ee001  36752  eel1111  36795  eel11111  36798  fnchoice  37038  fiiuncl  37096  mullimc  37316  islptre  37319  mullimcf  37323  addlimc  37349  stoweidlem20  37497  stoweidlem59  37537  perfectALTVlem2  38291
  Copyright terms: Public domain W3C validator