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

Theorem mpsyl 61
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 58 1  |-  ( ps 
->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  tbwlem1  1476  tbwlem2  1477  re1luk3  1483  merco1lem17  1504  re1tbw1  1516  a16gOLD  2013  onfr  4580  relcnvtr  5348  relresfld  5355  relcoi1  5357  foimacnv  5651  fvi  5742  isoini2  6018  ovidig  6150  frxp  6415  smores2  6575  mapdom1  7231  php2  7251  frfi  7311  fodomfi  7344  ixpfi2  7363  hartogs  7469  wemapso2lem  7475  card2on  7478  unwdomg  7508  r1pwss  7666  tz9.12lem3  7671  uniwf  7701  rankval3b  7708  tskwe  7793  carddomi2  7813  cardsdomelir  7816  infxpenlem  7851  inffien  7900  alephord  7912  alephdom  7918  iunfictbso  7951  dfac8  7971  dfacacn  7977  dfac13  7978  dfac12lem2  7980  infmap2  8054  ackbij1b  8075  ackbij2  8079  fictb  8081  cfslb  8102  fin67  8231  fin1a2lem10  8245  fin1a2lem11  8246  dcomex  8283  ttukeylem1  8345  ttukeylem7  8351  ondomon  8394  konigthlem  8399  alephadd  8408  alephexp1  8410  alephreg  8413  pwcfsdom  8414  fpwwe2lem13  8473  gchaleph  8506  gchaleph2  8507  winainflem  8524  inttsk  8605  inar1  8606  inatsk  8609  grudomon  8648  nqerid  8766  nqpr  8847  zmin  10526  uzrdgsuci  11255  limsupval2  12229  caucvgb  12428  sumz  12471  fsumsers  12477  isumclim  12496  isumnn0nn  12577  climcndslem1  12584  climcndslem2  12585  alzdvds  12854  bitsfzolem  12901  phicl2  13112  phibnd  13115  pclem  13167  strle1  13515  psss  14601  dprdss  15542  2ndcdisj  17472  dis2ndc  17476  hausmapdom  17516  ptcnplem  17606  fbun  17825  metrest  18507  opnreen  18815  bndth  18936  cmetcaulem  19194  ivthle  19306  ivthle2  19307  ovolfiniun  19350  volfiniun  19394  uniiccdif  19423  uniioovol  19424  uniioombllem4  19431  dyadmbl  19445  vitali  19458  mbfdm  19473  mbflimsup  19511  itg2monolem2  19596  itg2monolem3  19597  itg2mono  19598  cpnres  19776  dvcj  19789  dvef  19817  dvne0  19848  lhop2  19852  itgparts  19884  itgsubstlem  19885  ply1divex  20012  fta1blem  20044  dgrlem  20101  pige3  20378  xrlimcnp  20760  ftalem3  20810  lgsdchr  21085  dchrvmasumlem2  21145  pntlem3  21256  umgraex  21311  2trllemE  21506  0pthonv  21534  1pthon2v  21546  2pthon3v  21557  chscllem4  23095  adjeq  23391  hmopidmchi  23607  xreceu  24121  measvuni  24521  elmbfmvol2  24570  sibfof  24607  ballotlemfc0  24703  ballotlemfcc  24704  lgambdd  24774  iccllyscon  24890  cvmliftphtlem  24957  ntrivcvgfvn0  25180  ntrivcvgtail  25181  zprodn0  25218  iprodclim  25264  axcontlem2  25808  re1ax2lem  26036  re1ax2  26037  volsupnfl  26150  opnrebl2  26214  totbndbnd  26388  rabdiophlem1  26751  pellexlem5  26786  ttac  26997  aomclem4  27022  hbtlem5  27200  idomodle  27380  idomsubgmo  27382  ndmaovcl  27934  swrdccatin2  28018  swrdccatin12lem4  28025  swrdccatin12  28026  usg2wlk  28049  usg2wlkon  28050  vk15.4j  28323  a9e2nd  28356  eel0001  28539  trsspwALT2  28641  sspwtrALT  28644  sstrALT2  28656  a16gNEW7  29250  islsati  29477  hdmap14lem2a  32353
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator