MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl2im Structured version   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  1764  hbimdOLD  1835  ax12  2019  dvelimvOLD  2028  a16g  2048  a16gOLD  2049  equveli  2081  vtoclr  4914  funopg  5477  xpider  6967  undifixp  7090  onsdominel  7248  fodomr  7250  wemaplem2  7508  rankuni2b  7771  infxpenlem  7887  dfac8b  7904  ac10ct  7907  alephordi  7947  infdif  8081  cfflb  8131  alephval2  8439  tskxpss  8639  tskcard  8648  ingru  8682  grur1  8687  grothac  8697  suplem1pr  8921  mulgt0sr  8972  ixxssixx  10922  climrlim2  12333  qshash  12598  gcdcllem3  13005  vdwlem13  13353  opsrtoslem2  16537  ocvsscon  16894  txcnp  17644  t0kq  17842  filcon  17907  filuni  17909  alexsubALTlem3  18072  rectbntr0  18855  iscau4  19224  cfilres  19241  lmcau  19257  bcthlem2  19270  3v3e3cycl1  21623  4cycl4v4e  21645  4cycl4dv4e  21647  subfacp1lem6  24863  cvmsdisj  24949  meran1  26153  caushft  26458  harinf  27096  onfrALTlem3  28567  onfrALTlem2  28569  e222  28674  e111  28712  e333  28782  bitr3VD  28898  dvelimvNEW7  29399  a16gNEW7  29483
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator