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

Theorem syl3c 57
Description: A syllogism inference combined with contraction. e111 28199 without virtual deductions. (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 56 . 2  |-  ( ph  ->  ( th  ->  ta ) )
61, 5mpd 14 1  |-  ( ph  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  fodomr  7155  dffi3  7331  cantnflt  7520  cantnflem1c  7536  cantnflem1  7538  isfin2-2  8092  fin23lem17  8111  fin23lem39  8123  axdc3lem2  8224  ttukeylem5  8287  pwfseqlem5  8432  seqf1olem2  11250  wrdind  11678  rlimclim1  12226  caucvgrlem  12353  o1fsum  12479  prmind2  12977  rami  13270  ramcl  13284  poslubmo  14460  pslem  14525  pgpfaclem2  15527  islbs3  16118  mplsubglem  16389  mpllsslem  16390  prmirredlem  16663  lmcvg  17209  lmff  17246  lmmo  17325  1stcfb  17388  1stcelcls  17404  restnlly  17425  lly1stc  17439  kgeni  17449  cnmpt12  17578  cnmpt22  17585  filss  17761  flimopn  17883  flimrest  17891  tgpt0  18014  tsmsi  18029  tsmsxp  18050  nmoleub2lem2  18812  nmoleub3  18815  cfil3i  18910  equivcfil  18940  equivcau  18941  ovolicc2lem3  19093  ovolicc2  19096  vitalilem2  19179  vitalilem3  19180  itg2seq  19312  limciun  19459  dvferm1lem  19546  dvferm2lem  19548  dvcnvrelem1  19579  dvfsumrlim  19593  dvfsum2  19596  ftc1a  19599  ftc1lem4  19601  fta1glem2  19767  plyeq0lem  19807  dgrcolem2  19870  dgrco  19871  plydivlem4  19891  fta1lem  19902  vieta1  19907  scvxcvx  20502  wilthlem2  20530  ftalem3  20535  perfectlem2  20692  2sqlem6  20831  2sqlem8  20834  dchrisumlema  20860  dchrisumlem2  20862  pjoi0  22609  atomli  23275  sigaclcu  23965  measvun  24026  relexpindlem  24623  relexpind  24624  rtrclind  24633  ftc1cnnclem  25696  neibastop2lem  25816  sdclem2  25959  heibor1lem  26039  ismrcd1  26279  pthdepisspth  27718  ee222  28010  ee333  28015  ee1111  28025  sbcoreleleq  28045  ordelordALT  28048  trsbc  28051  ee110  28202  ee101  28204  ee011  28206  ee100  28208  ee010  28210  ee001  28212  bnj1128  28784  bnj1204  28806  bnj1417  28835  cvrat4  29703  hdmapval2  32096
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator