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 28493 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  7225  dffi3  7402  cantnflt  7591  cantnflem1c  7607  cantnflem1  7609  isfin2-2  8163  fin23lem17  8182  fin23lem39  8194  axdc3lem2  8295  ttukeylem5  8357  pwfseqlem5  8502  seqf1olem2  11326  wrdind  11754  rlimclim1  12302  caucvgrlem  12429  o1fsum  12555  prmind2  13053  rami  13346  ramcl  13360  poslubmo  14536  pslem  14601  pgpfaclem2  15603  islbs3  16190  mplsubglem  16461  mpllsslem  16462  prmirredlem  16736  lmcvg  17288  lmff  17327  lmmo  17406  1stcfb  17469  1stcelcls  17485  restnlly  17506  lly1stc  17520  kgeni  17530  cnmpt12  17660  cnmpt22  17667  filss  17846  flimopn  17968  flimrest  17976  tgpt0  18109  tsmsi  18124  tsmsxp  18145  nmoleub2lem2  19085  nmoleub3  19088  cfil3i  19183  equivcfil  19213  equivcau  19214  ovolicc2lem3  19376  ovolicc2  19379  vitalilem2  19462  vitalilem3  19463  itg2seq  19595  limciun  19742  dvferm1lem  19829  dvferm2lem  19831  dvcnvrelem1  19862  dvfsumrlim  19876  dvfsum2  19879  ftc1a  19882  ftc1lem4  19884  fta1glem2  20050  plyeq0lem  20090  dgrcolem2  20153  dgrco  20154  plydivlem4  20174  fta1lem  20185  vieta1  20190  scvxcvx  20785  wilthlem2  20813  ftalem3  20818  perfectlem2  20975  2sqlem6  21114  2sqlem8  21117  dchrisumlema  21143  dchrisumlem2  21145  pthdepisspth  21535  pjoi0  23180  atomli  23846  sigaclcu  24461  measvun  24524  relexpindlem  25100  relexpind  25101  rtrclind  25110  ftc1cnnclem  26185  neibastop2lem  26287  sdclem2  26344  heibor1lem  26416  ismrcd1  26650  fnchoice  27575  stoweidlem20  27644  stoweidlem59  27683  ee222  28303  ee333  28308  ee1111  28318  sbcoreleleq  28338  ordelordALT  28341  trsbc  28344  ee110  28496  ee101  28498  ee011  28500  ee100  28502  ee010  28504  ee001  28506  eel1111  28550  eel11111  28553  bnj1128  29077  bnj1204  29099  bnj1417  29128  cvrat4  29937  hdmapval2  32330
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator