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

Theorem syl3c 59
Description: A syllogism inference combined with contraction. e111 28484 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 58 . 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  7217  dffi3  7394  cantnflt  7583  cantnflem1c  7599  cantnflem1  7601  isfin2-2  8155  fin23lem17  8174  fin23lem39  8186  axdc3lem2  8287  ttukeylem5  8349  pwfseqlem5  8494  seqf1olem2  11318  wrdind  11746  rlimclim1  12294  caucvgrlem  12421  o1fsum  12547  prmind2  13045  rami  13338  ramcl  13352  poslubmo  14528  pslem  14593  pgpfaclem2  15595  islbs3  16182  mplsubglem  16453  mpllsslem  16454  prmirredlem  16728  lmcvg  17280  lmff  17319  lmmo  17398  1stcfb  17461  1stcelcls  17477  restnlly  17498  lly1stc  17512  kgeni  17522  cnmpt12  17652  cnmpt22  17659  filss  17838  flimopn  17960  flimrest  17968  tgpt0  18101  tsmsi  18116  tsmsxp  18137  nmoleub2lem2  19077  nmoleub3  19080  cfil3i  19175  equivcfil  19205  equivcau  19206  ovolicc2lem3  19368  ovolicc2  19371  vitalilem2  19454  vitalilem3  19455  itg2seq  19587  limciun  19734  dvferm1lem  19821  dvferm2lem  19823  dvcnvrelem1  19854  dvfsumrlim  19868  dvfsum2  19871  ftc1a  19874  ftc1lem4  19876  fta1glem2  20042  plyeq0lem  20082  dgrcolem2  20145  dgrco  20146  plydivlem4  20166  fta1lem  20177  vieta1  20182  scvxcvx  20777  wilthlem2  20805  ftalem3  20810  perfectlem2  20967  2sqlem6  21106  2sqlem8  21109  dchrisumlema  21135  dchrisumlem2  21137  pthdepisspth  21527  pjoi0  23172  atomli  23838  sigaclcu  24453  measvun  24516  relexpindlem  25092  relexpind  25093  rtrclind  25102  ftc1cnnclem  26177  neibastop2lem  26279  sdclem2  26336  heibor1lem  26408  ismrcd1  26642  fnchoice  27567  stoweidlem20  27636  stoweidlem59  27675  ee222  28295  ee333  28300  ee1111  28310  sbcoreleleq  28330  ordelordALT  28333  trsbc  28336  ee110  28487  ee101  28489  ee011  28491  ee100  28493  ee010  28495  ee001  28497  eel1111  28541  eel11111  28544  bnj1128  29065  bnj1204  29087  bnj1417  29116  cvrat4  29925  hdmapval2  32318
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator