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

Theorem syl3c 62
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 61 . 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  7112  fodomr  7741  dffi3  7963  cantnflt  8195  cantnflem1c  8210  cantnflem1  8212  isfin2-2  8767  fin23lem17  8786  fin23lem39  8798  axdc3lem2  8899  ttukeylem5  8961  pwfseqlem5  9106  seqf1olem2  12291  wrdind  12887  wrd2ind  12888  relexpindlem  13203  rtrclind  13205  rlimclim1  13686  caucvgrlem  13813  caucvgrlemOLD  13814  o1fsum  13950  lcmneg  14647  prmind2  14714  rami  15051  ramcl  15066  poslubmo  16470  posglbmo  16471  pslem  16530  telgsums  17701  pgpfaclem2  17793  islbs3  18456  mplsubglem  18735  mpllsslem  18736  prmirredlem  19141  psgndif  19247  gsummatr01lem4  19760  lmcvg  20355  lmff  20394  lmmo  20473  1stcfb  20537  1stcelcls  20553  restnlly  20574  lly1stc  20588  kgeni  20629  cnmpt12  20759  cnmpt22  20766  filss  20946  flimopn  21068  flimrest  21076  tgpt0  21211  tsmsi  21226  tsmsxp  21247  nmoleub2lem2  22208  nmoleub3  22211  cfil3i  22317  equivcfil  22347  equivcau  22348  ovolicc2lem3  22550  ovolicc2  22554  vitalilem2  22646  vitalilem3  22647  itg2seq  22779  limciun  22928  dvferm1lem  23015  dvferm2lem  23017  dvcnvrelem1  23048  dvfsumrlim  23062  dvfsum2  23065  ftc1a  23068  ftc1lem4  23070  fta1glem2  23196  plyeq0lem  23243  dgrcolem2  23307  dgrco  23308  plydivlem4  23328  fta1lem  23339  vieta1  23344  scvxcvx  23990  wilthlem2  24073  ftalem3  24078  perfectlem2  24237  2sqlem6  24376  2sqlem8  24379  dchrisumlema  24405  dchrisumlem2  24407  pthdepisspth  25383  pjoi0  27451  atomli  28116  archirng  28579  archiabllem1a  28582  archiabllem2a  28585  archiabl  28589  crefi  28748  pcmplfin  28761  sigaclcu  29013  measvun  29105  signsply0  29512  bnj1128  29871  bnj1204  29893  bnj1417  29922  neibastop2lem  31087  poimirlem31  32035  ftc1cnnclem  32079  sdclem2  32135  heibor1lem  32205  cvrat4  33079  hdmapval2  35474  ismrcd1  35611  relexpxpmin  36380  ee222  36928  ee333  36933  ee1111  36943  sbcoreleleq  36966  ordelordALT  36968  trsbc  36971  ee110  37124  ee101  37126  ee011  37128  ee100  37130  ee010  37132  ee001  37134  eel1111  37170  eel11111  37173  fnchoice  37413  fiiuncl  37465  mullimc  37793  islptre  37796  mullimcf  37800  addlimc  37826  stoweidlem20  37992  stoweidlem59  38032  perfectALTVlem2  38989  gropd  39286  grstructd  39287  pthdepissPth  39927
  Copyright terms: Public domain W3C validator