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

Theorem syl3c 61
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 60 . 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  6821  fodomr  7450  dffi3  7669  cantnflt  7868  cantnflem1c  7883  cantnflem1  7885  cantnfltOLD  7898  cantnflem1cOLD  7906  cantnflem1OLD  7908  isfin2-2  8476  fin23lem17  8495  fin23lem39  8507  axdc3lem2  8608  ttukeylem5  8670  pwfseqlem5  8817  seqf1olem2  11829  wrdind  12354  wrd2ind  12355  rlimclim1  13006  caucvgrlem  13133  o1fsum  13258  prmind2  13756  rami  14058  ramcl  14072  poslubmo  15298  posglbmo  15299  pslem  15358  pgpfaclem2  16556  islbs3  17157  mplsubglem  17443  mpllsslem  17444  mplsubglemOLD  17445  mpllsslemOLD  17446  prmirredlem  17758  prmirredlemOLD  17761  psgndif  17873  gsummatr01lem4  18305  lmcvg  18707  lmff  18746  lmmo  18825  1stcfb  18890  1stcelcls  18906  restnlly  18927  lly1stc  18941  kgeni  18951  cnmpt12  19081  cnmpt22  19088  filss  19267  flimopn  19389  flimrest  19397  tgpt0  19530  tsmsi  19545  tsmsxp  19570  nmoleub2lem2  20512  nmoleub3  20515  cfil3i  20621  equivcfil  20651  equivcau  20652  ovolicc2lem3  20843  ovolicc2  20846  vitalilem2  20930  vitalilem3  20931  itg2seq  21061  limciun  21210  dvferm1lem  21297  dvferm2lem  21299  dvcnvrelem1  21330  dvfsumrlim  21344  dvfsum2  21347  ftc1a  21350  ftc1lem4  21352  fta1glem2  21522  plyeq0lem  21562  dgrcolem2  21625  dgrco  21626  plydivlem4  21646  fta1lem  21657  vieta1  21662  scvxcvx  22263  wilthlem2  22291  ftalem3  22296  perfectlem2  22453  2sqlem6  22592  2sqlem8  22595  dchrisumlema  22621  dchrisumlem2  22623  pthdepisspth  23295  pjoi0  24942  atomli  25608  archiabllem1a  26031  archiabllem2a  26034  sigaclcu  26413  measvun  26476  relexpindlem  27187  relexpind  27188  rtrclind  27197  ftc1cnnclem  28306  neibastop2lem  28422  sdclem2  28479  heibor1lem  28549  ismrcd1  28876  fnchoice  29593  stoweidlem20  29658  stoweidlem59  29697  ee222  30904  ee333  30909  ee1111  30919  sbcoreleleq  30939  ordelordALT  30942  trsbc  30945  ee110  31098  ee101  31100  ee011  31102  ee100  31104  ee010  31106  ee001  31108  eel1111  31152  eel11111  31155  bnj1128  31680  bnj1204  31702  bnj1417  31731  cvrat4  32657  hdmapval2  35050
  Copyright terms: Public domain W3C validator