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

Theorem syl2im 36
Description: Replace two antecedents. Implication-only version of syl2an 464. (Contributed by Wolf Lammen, 14-May-2013.)
Hypotheses
Ref Expression
syl2im.1  |-  ( ph  ->  ps )
syl2im.2  |-  ( ch 
->  th )
syl2im.3  |-  ( ps 
->  ( th  ->  ta ) )
Assertion
Ref Expression
syl2im  |-  ( ph  ->  ( ch  ->  ta ) )

Proof of Theorem syl2im
StepHypRef Expression
1 syl2im.1 . 2  |-  ( ph  ->  ps )
2 syl2im.2 . . 3  |-  ( ch 
->  th )
3 syl2im.3 . . 3  |-  ( ps 
->  ( th  ->  ta ) )
42, 3syl5 30 . 2  |-  ( ps 
->  ( ch  ->  ta ) )
51, 4syl 16 1  |-  ( ph  ->  ( ch  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  sylc  58  bi3ant  281  spOLD  1760  hbimdOLD  1831  ax12  1985  dvelimvOLD  1994  a16g  2012  a16gOLD  2013  equveli  2042  vtoclr  4881  funopg  5444  xpider  6934  undifixp  7057  onsdominel  7215  fodomr  7217  wemaplem2  7472  rankuni2b  7735  infxpenlem  7851  dfac8b  7868  ac10ct  7871  alephordi  7911  infdif  8045  cfflb  8095  alephval2  8403  tskxpss  8603  tskcard  8612  ingru  8646  grur1  8651  grothac  8661  suplem1pr  8885  mulgt0sr  8936  ixxssixx  10886  climrlim2  12296  qshash  12561  gcdcllem3  12968  vdwlem13  13316  opsrtoslem2  16500  ocvsscon  16857  txcnp  17605  t0kq  17803  filcon  17868  filuni  17870  alexsubALTlem3  18033  rectbntr0  18816  iscau4  19185  cfilres  19202  lmcau  19218  bcthlem2  19231  3v3e3cycl1  21584  4cycl4v4e  21606  4cycl4dv4e  21608  subfacp1lem6  24824  cvmsdisj  24910  meran1  26065  caushft  26357  harinf  26995  swrdccatin12lem3b  28022  onfrALTlem3  28341  onfrALTlem2  28343  e222  28446  e111  28484  e333  28554  bitr3VD  28670  dvelimvNEW7  29168  a16gNEW7  29250
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator