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  1716  hbimd  1721  dvelimv  1879  a16g  1885  vtoclr  4733  funopg  5286  xpider  6730  undifixp  6852  onsdominel  7010  fodomr  7012  wemaplem2  7262  rankuni2b  7525  infxpenlem  7641  dfac8b  7658  ac10ct  7661  alephordi  7701  infdif  7835  cfflb  7885  alephval2  8194  tskxpss  8394  tskcard  8403  ingru  8437  grur1  8442  grothac  8452  suplem1pr  8676  mulgt0sr  8727  ixxssixx  10670  climrlim2  12021  qshash  12285  gcdcllem3  12692  vdwlem13  13040  opsrtoslem2  16226  ocvsscon  16575  txcnp  17314  t0kq  17509  filcon  17578  filuni  17580  alexsubALTlem3  17743  rectbntr0  18337  iscau4  18705  cfilres  18722  lmcau  18738  bcthlem2  18747  subfacp1lem6  23716  cvmsdisj  23801  meran1  24850  oooeqim2  25053  reflincror  25112  valcurfn1  25204  rngmgmbs3  25417  rngodmeqrn  25419  fldi  25427  eqidob  25795  prismorcsetlemc  25917  caushft  26477  harinf  27127  onfrALTlem3  28309  onfrALTlem2  28311  e222  28408  e111  28446  e333  28508  bitr3VD  28625  ax10lem17ALT  29123  ax9lem2  29141  ax9lem3  29142  ax9lem9  29148  ax9lem15  29154  ax9lem17  29156
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator