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

Theorem syl3c 63
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 62 . 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  7091  fodomr  7720  dffi3  7942  cantnflt  8174  cantnflem1c  8189  cantnflem1  8191  isfin2-2  8746  fin23lem17  8765  fin23lem39  8777  axdc3lem2  8878  ttukeylem5  8940  pwfseqlem5  9085  seqf1olem2  12250  wrdind  12828  wrd2ind  12829  relexpindlem  13119  rtrclind  13121  rlimclim1  13602  caucvgrlem  13729  caucvgrlemOLD  13730  o1fsum  13866  lcmneg  14561  prmind2  14628  rami  14965  ramcl  14980  poslubmo  16385  posglbmo  16386  pslem  16445  telgsums  17616  pgpfaclem2  17708  islbs3  18371  mplsubglem  18651  mpllsslem  18652  prmirredlem  19057  psgndif  19163  gsummatr01lem4  19676  lmcvg  20271  lmff  20310  lmmo  20389  1stcfb  20453  1stcelcls  20469  restnlly  20490  lly1stc  20504  kgeni  20545  cnmpt12  20675  cnmpt22  20682  filss  20861  flimopn  20983  flimrest  20991  tgpt0  21126  tsmsi  21141  tsmsxp  21162  nmoleub2lem2  22123  nmoleub3  22126  cfil3i  22232  equivcfil  22262  equivcau  22263  ovolicc2lem3  22465  ovolicc2  22469  vitalilem2  22560  vitalilem3  22561  itg2seq  22693  limciun  22842  dvferm1lem  22929  dvferm2lem  22931  dvcnvrelem1  22962  dvfsumrlim  22976  dvfsum2  22979  ftc1a  22982  ftc1lem4  22984  fta1glem2  23110  plyeq0lem  23157  dgrcolem2  23221  dgrco  23222  plydivlem4  23242  fta1lem  23253  vieta1  23258  scvxcvx  23904  wilthlem2  23987  ftalem3  23992  perfectlem2  24151  2sqlem6  24290  2sqlem8  24293  dchrisumlema  24319  dchrisumlem2  24321  pthdepisspth  25297  pjoi0  27363  atomli  28028  archirng  28498  archiabllem1a  28501  archiabllem2a  28504  archiabl  28508  crefi  28667  pcmplfin  28680  sigaclcu  28932  measvun  29024  signsply0  29433  bnj1128  29792  bnj1204  29814  bnj1417  29843  neibastop2lem  31009  poimirlem31  31964  ftc1cnnclem  32008  sdclem2  32064  heibor1lem  32134  cvrat4  33002  hdmapval2  35397  ismrcd1  35534  relexpxpmin  36303  ee222  36852  ee333  36857  ee1111  36867  sbcoreleleq  36890  ordelordALT  36892  trsbc  36895  ee110  37050  ee101  37052  ee011  37054  ee100  37056  ee010  37058  ee001  37060  eel1111  37101  eel11111  37104  fnchoice  37344  fiiuncl  37400  mullimc  37690  islptre  37693  mullimcf  37697  addlimc  37723  stoweidlem20  37874  stoweidlem59  37914  perfectALTVlem2  38838  gropd  39119  grstructd  39120
  Copyright terms: Public domain W3C validator