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  7045  fodomr  7668  dffi3  7891  cantnflt  8091  cantnflem1c  8106  cantnflem1  8108  cantnfltOLD  8121  cantnflem1cOLD  8129  cantnflem1OLD  8131  isfin2-2  8699  fin23lem17  8718  fin23lem39  8730  axdc3lem2  8831  ttukeylem5  8893  pwfseqlem5  9041  seqf1olem2  12115  wrdind  12665  wrd2ind  12666  rlimclim1  13331  caucvgrlem  13458  o1fsum  13590  prmind2  14087  rami  14392  ramcl  14406  poslubmo  15633  posglbmo  15634  pslem  15693  telgsums  16825  pgpfaclem2  16935  islbs3  17601  mplsubglem  17892  mpllsslem  17893  mplsubglemOLD  17894  mpllsslemOLD  17895  prmirredlem  18318  prmirredlemOLD  18321  psgndif  18433  gsummatr01lem4  18955  lmcvg  19557  lmff  19596  lmmo  19675  1stcfb  19740  1stcelcls  19756  restnlly  19777  lly1stc  19791  kgeni  19801  cnmpt12  19931  cnmpt22  19938  filss  20117  flimopn  20239  flimrest  20247  tgpt0  20380  tsmsi  20395  tsmsxp  20420  nmoleub2lem2  21362  nmoleub3  21365  cfil3i  21471  equivcfil  21501  equivcau  21502  ovolicc2lem3  21693  ovolicc2  21696  vitalilem2  21781  vitalilem3  21782  itg2seq  21912  limciun  22061  dvferm1lem  22148  dvferm2lem  22150  dvcnvrelem1  22181  dvfsumrlim  22195  dvfsum2  22198  ftc1a  22201  ftc1lem4  22203  fta1glem2  22330  plyeq0lem  22370  dgrcolem2  22433  dgrco  22434  plydivlem4  22454  fta1lem  22465  vieta1  22470  scvxcvx  23071  wilthlem2  23099  ftalem3  23104  perfectlem2  23261  2sqlem6  23400  2sqlem8  23403  dchrisumlema  23429  dchrisumlem2  23431  pthdepisspth  24280  pjoi0  26339  atomli  27005  archiabllem1a  27425  archiabllem2a  27428  sigaclcu  27785  measvun  27848  relexpindlem  28565  relexpind  28566  rtrclind  28575  ftc1cnnclem  29693  neibastop2lem  29809  sdclem2  29866  heibor1lem  29936  ismrcd1  30262  lcmneg  30837  fnchoice  31010  mullimc  31186  mullimcf  31193  stoweidlem20  31348  stoweidlem59  31387  ee222  32368  ee333  32373  ee1111  32383  sbcoreleleq  32403  ordelordALT  32406  trsbc  32409  ee110  32561  ee101  32563  ee011  32565  ee100  32567  ee010  32569  ee001  32571  eel1111  32615  eel11111  32618  bnj1128  33143  bnj1204  33165  bnj1417  33194  cvrat4  34257  hdmapval2  36650
  Copyright terms: Public domain W3C validator