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  1756  hbimdOLD  1825  ax12  1973  dvelimvOLD  1985  a16g  1992  a16gOLD  1993  vtoclr  4862  funopg  5425  xpider  6911  undifixp  7034  onsdominel  7192  fodomr  7194  wemaplem2  7449  rankuni2b  7712  infxpenlem  7828  dfac8b  7845  ac10ct  7848  alephordi  7888  infdif  8022  cfflb  8072  alephval2  8380  tskxpss  8580  tskcard  8589  ingru  8623  grur1  8628  grothac  8638  suplem1pr  8862  mulgt0sr  8913  ixxssixx  10862  climrlim2  12268  qshash  12533  gcdcllem3  12940  vdwlem13  13288  opsrtoslem2  16472  ocvsscon  16825  txcnp  17573  t0kq  17771  filcon  17836  filuni  17838  alexsubALTlem3  18001  rectbntr0  18734  iscau4  19103  cfilres  19120  lmcau  19136  bcthlem2  19147  3v3e3cycl1  21479  4cycl4v4e  21501  4cycl4dv4e  21503  subfacp1lem6  24650  cvmsdisj  24736  meran1  25875  caushft  26158  harinf  26796  onfrALTlem3  27973  onfrALTlem2  27975  e222  28078  e111  28116  e333  28186  bitr3VD  28302  dvelimvNEW7  28800  a16gNEW7  28882
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator