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 28446 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  7012  dffi3  7184  cantnflt  7373  cantnflem1c  7389  cantnflem1  7391  isfin2-2  7945  fin23lem17  7964  fin23lem39  7976  axdc3lem2  8077  ttukeylem5  8140  pwfseqlem5  8285  seqf1olem2  11086  wrdind  11477  rlimclim1  12019  caucvgrlem  12145  o1fsum  12271  prmind2  12769  rami  13062  ramcl  13076  poslubmo  14250  pslem  14315  pgpfaclem2  15317  islbs3  15908  mplsubglem  16179  mpllsslem  16180  prmirredlem  16446  lmcvg  16992  lmff  17029  lmmo  17108  1stcfb  17171  1stcelcls  17187  restnlly  17208  lly1stc  17222  kgeni  17232  cnmpt12  17361  cnmpt22  17368  filss  17548  flimopn  17670  flimrest  17678  tgpt0  17801  tsmsi  17816  tsmsxp  17837  nmoleub2lem2  18597  nmoleub3  18600  cfil3i  18695  equivcfil  18725  equivcau  18726  ovolicc2lem3  18878  ovolicc2  18881  vitalilem2  18964  vitalilem3  18965  itg2seq  19097  limciun  19244  dvferm1lem  19331  dvferm2lem  19333  dvcnvrelem1  19364  dvfsumrlim  19378  dvfsum2  19381  ftc1a  19384  ftc1lem4  19386  fta1glem2  19552  plyeq0lem  19592  dgrcolem2  19655  dgrco  19656  plydivlem4  19676  fta1lem  19687  vieta1  19692  scvxcvx  20280  wilthlem2  20307  ftalem3  20312  perfectlem2  20469  2sqlem6  20608  2sqlem8  20611  dchrisumlema  20637  dchrisumlem2  20639  pjoi0  22296  atomli  22962  sigaclcu  23478  measvun  23537  relexpindlem  24036  relexpind  24037  rtrclind  24046  neibastop2lem  26309  sdclem2  26452  heibor1lem  26533  ismrcd1  26773  ee222  28263  ee333  28268  ee1111  28278  sbcoreleleq  28298  ordelordALT  28301  trsbc  28304  ee110  28449  ee101  28451  ee011  28453  ee100  28455  ee010  28457  ee001  28459  bnj1128  29020  bnj1204  29042  bnj1417  29071  cvrat4  29632  hdmapval2  32025
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator