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

Theorem syl3c 60
Description: A syllogism inference combined with contraction. e111 28837 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 59 . 2  |-  ( ph  ->  ( th  ->  ta ) )
61, 5mpd 15 1  |-  ( ph  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  fodomr  7260  dffi3  7438  cantnflt  7629  cantnflem1c  7645  cantnflem1  7647  isfin2-2  8201  fin23lem17  8220  fin23lem39  8232  axdc3lem2  8333  ttukeylem5  8395  pwfseqlem5  8540  seqf1olem2  11365  wrdind  11793  rlimclim1  12341  caucvgrlem  12468  o1fsum  12594  prmind2  13092  rami  13385  ramcl  13399  poslubmo  14575  pslem  14640  pgpfaclem2  15642  islbs3  16229  mplsubglem  16500  mpllsslem  16501  prmirredlem  16775  lmcvg  17328  lmff  17367  lmmo  17446  1stcfb  17510  1stcelcls  17526  restnlly  17547  lly1stc  17561  kgeni  17571  cnmpt12  17701  cnmpt22  17708  filss  17887  flimopn  18009  flimrest  18017  tgpt0  18150  tsmsi  18165  tsmsxp  18186  nmoleub2lem2  19126  nmoleub3  19129  cfil3i  19224  equivcfil  19254  equivcau  19255  ovolicc2lem3  19417  ovolicc2  19420  vitalilem2  19503  vitalilem3  19504  itg2seq  19636  limciun  19783  dvferm1lem  19870  dvferm2lem  19872  dvcnvrelem1  19903  dvfsumrlim  19917  dvfsum2  19920  ftc1a  19923  ftc1lem4  19925  fta1glem2  20091  plyeq0lem  20131  dgrcolem2  20194  dgrco  20195  plydivlem4  20215  fta1lem  20226  vieta1  20231  scvxcvx  20826  wilthlem2  20854  ftalem3  20859  perfectlem2  21016  2sqlem6  21155  2sqlem8  21158  dchrisumlema  21184  dchrisumlem2  21186  pthdepisspth  21576  pjoi0  23221  atomli  23887  sigaclcu  24502  measvun  24565  relexpindlem  25141  relexpind  25142  rtrclind  25151  ftc1cnnclem  26280  neibastop2lem  26391  sdclem2  26448  heibor1lem  26520  ismrcd1  26754  fnchoice  27678  stoweidlem20  27747  stoweidlem59  27786  ee222  28646  ee333  28651  ee1111  28661  sbcoreleleq  28681  ordelordALT  28684  trsbc  28687  ee110  28840  ee101  28842  ee011  28844  ee100  28846  ee010  28848  ee001  28850  eel1111  28894  eel11111  28897  bnj1128  29421  bnj1204  29443  bnj1417  29472  cvrat4  30302  hdmapval2  32695
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator