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

Theorem mpsyl 62
Description: Modus ponens combined with a syllogism inference. (Contributed by Alan Sare, 20-Apr-2011.)
Hypotheses
Ref Expression
mpsyl.1  |-  ph
mpsyl.2  |-  ( ps 
->  ch )
mpsyl.3  |-  ( ph  ->  ( ch  ->  th )
)
Assertion
Ref Expression
mpsyl  |-  ( ps 
->  th )

Proof of Theorem mpsyl
StepHypRef Expression
1 mpsyl.1 . . 3  |-  ph
21a1i 11 . 2  |-  ( ps 
->  ph )
3 mpsyl.2 . 2  |-  ( ps 
->  ch )
4 mpsyl.3 . 2  |-  ( ph  ->  ( ch  ->  th )
)
52, 3, 4sylc 59 1  |-  ( ps 
->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  tbwlem1  1480  tbwlem2  1481  re1luk3  1487  merco1lem17  1508  re1tbw1  1520  a16gOLD  2050  onfr  4622  relcnvtr  5391  relresfld  5398  relcoi1  5400  foimacnv  5694  fvi  5785  isoini2  6061  ovidig  6193  frxp  6458  smores2  6618  mapdom1  7274  php2  7294  frfi  7354  fodomfi  7387  ixpfi2  7407  hartogs  7515  wemapso2lem  7521  card2on  7524  unwdomg  7554  r1pwss  7712  tz9.12lem3  7717  uniwf  7747  rankval3b  7754  tskwe  7839  carddomi2  7859  cardsdomelir  7862  infxpenlem  7897  inffien  7946  alephord  7958  alephdom  7964  iunfictbso  7997  dfac8  8017  dfacacn  8023  dfac13  8024  dfac12lem2  8026  infmap2  8100  ackbij1b  8121  ackbij2  8125  fictb  8127  cfslb  8148  fin67  8277  fin1a2lem10  8291  fin1a2lem11  8292  dcomex  8329  ttukeylem1  8391  ttukeylem7  8397  ondomon  8440  konigthlem  8445  alephadd  8454  alephexp1  8456  alephreg  8459  pwcfsdom  8460  fpwwe2lem13  8519  gchaleph  8552  gchaleph2  8553  winainflem  8570  inttsk  8651  inar1  8652  inatsk  8655  grudomon  8694  nqerid  8812  nqpr  8893  zmin  10572  uzrdgsuci  11302  limsupval2  12276  caucvgb  12475  sumz  12518  fsumsers  12524  isumclim  12543  isumnn0nn  12624  climcndslem1  12631  climcndslem2  12632  alzdvds  12901  bitsfzolem  12948  phicl2  13159  phibnd  13162  pclem  13214  strle1  13562  psss  14648  dprdss  15589  2ndcdisj  17521  dis2ndc  17525  hausmapdom  17565  ptcnplem  17655  fbun  17874  metrest  18556  opnreen  18864  bndth  18985  cmetcaulem  19243  ivthle  19355  ivthle2  19356  ovolfiniun  19399  volfiniun  19443  uniiccdif  19472  uniioovol  19473  uniioombllem4  19480  dyadmbl  19494  vitali  19507  mbfdm  19522  mbflimsup  19560  itg2monolem2  19645  itg2monolem3  19646  itg2mono  19647  cpnres  19825  dvcj  19838  dvef  19866  dvne0  19897  lhop2  19901  itgparts  19933  itgsubstlem  19934  ply1divex  20061  fta1blem  20093  dgrlem  20150  pige3  20427  xrlimcnp  20809  ftalem3  20859  lgsdchr  21134  dchrvmasumlem2  21194  pntlem3  21305  umgraex  21360  2trllemE  21555  0pthonv  21583  1pthon2v  21595  2pthon3v  21606  chscllem4  23144  adjeq  23440  hmopidmchi  23656  xreceu  24170  measvuni  24570  elmbfmvol2  24619  sibfof  24656  ballotlemfc0  24752  ballotlemfcc  24753  lgambdd  24823  iccllyscon  24939  cvmliftphtlem  25006  ntrivcvgfvn0  25229  ntrivcvgtail  25230  zprodn0  25267  iprodclim  25313  axcontlem2  25906  re1ax2lem  26134  re1ax2  26135  volsupnfl  26253  areacirc  26299  opnrebl2  26326  totbndbnd  26500  rabdiophlem1  26863  pellexlem5  26898  ttac  27109  aomclem4  27134  hbtlem5  27311  idomodle  27491  idomsubgmo  27493  ndmaovcl  28045  swrdccatin12lem4  28235  usg2wlk  28345  usg2wlkon  28346  vk15.4j  28674  a9e2nd  28707  eel0001  28892  trsspwALT2  28994  sspwtrALT  28997  sstrALT2  29009  a16gNEW7  29608  islsati  29854  hdmap14lem2a  32730
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator