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

Theorem syl2im 34
Description: Replace two antecedents. Implication-only version of syl2an 463. (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 28 . 2  |-  ( ps 
->  ( ch  ->  ta ) )
51, 4syl 15 1  |-  ( ph  ->  ( ch  ->  ta ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  sylc  56  bi3ant  280  sp  1728  hbimd  1733  dvelimv  1892  a16g  1898  vtoclr  4749  funopg  5302  xpider  6746  undifixp  6868  onsdominel  7026  fodomr  7028  wemaplem2  7278  rankuni2b  7541  infxpenlem  7657  dfac8b  7674  ac10ct  7677  alephordi  7717  infdif  7851  cfflb  7901  alephval2  8210  tskxpss  8410  tskcard  8419  ingru  8453  grur1  8458  grothac  8468  suplem1pr  8692  mulgt0sr  8743  ixxssixx  10686  climrlim2  12037  qshash  12301  gcdcllem3  12708  vdwlem13  13056  opsrtoslem2  16242  ocvsscon  16591  txcnp  17330  t0kq  17525  filcon  17594  filuni  17596  alexsubALTlem3  17759  rectbntr0  18353  iscau4  18721  cfilres  18738  lmcau  18754  bcthlem2  18763  subfacp1lem6  23731  cvmsdisj  23816  meran1  24922  oooeqim2  25156  reflincror  25215  valcurfn1  25307  rngmgmbs3  25520  rngodmeqrn  25522  fldi  25530  eqidob  25898  prismorcsetlemc  26020  caushft  26580  harinf  27230  3v3e3cycl1  28390  4cycl4v4e  28412  4cycl4dv4e  28414  onfrALTlem3  28608  onfrALTlem2  28610  e222  28713  e111  28751  e333  28822  bitr3VD  28941  dvelimvNEW7  29439  a16gNEW7  29521  ax10lem17ALT  29745  ax9lem2  29763  ax9lem3  29764  ax9lem9  29770  ax9lem15  29776  ax9lem17  29778
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator