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

Theorem mpsyl 59
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 10 . 2  |-  ( ps 
->  ph )
3 mpsyl.2 . 2  |-  ( ps 
->  ch )
4 mpsyl.3 . 2  |-  ( ph  ->  ( ch  ->  th )
)
52, 3, 4sylc 56 1  |-  ( ps 
->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  tbwlem1  1460  tbwlem2  1461  re1luk3  1467  merco1lem17  1488  re1tbw1  1500  a16g  1898  relcnvtr  5208  relresfld  5215  relcoi1  5217  foimacnv  5506  fvi  5595  isoini2  5852  ovidig  5981  frxp  6241  smores2  6387  mapdom1  7042  php2  7062  frfi  7118  fodomfi  7151  ixpfi2  7170  hartogs  7275  wemapso2lem  7281  card2on  7284  unwdomg  7314  r1pwss  7472  tz9.12lem3  7477  uniwf  7507  rankval3b  7514  tskwe  7599  carddomi2  7619  cardsdomelir  7622  infxpenlem  7657  inffien  7706  alephord  7718  alephdom  7724  iunfictbso  7757  dfac8  7777  dfacacn  7783  dfac13  7784  dfac12lem2  7786  infmap2  7860  ackbij1b  7881  ackbij2  7885  fictb  7887  cfslb  7908  fin67  8037  fin1a2lem10  8051  fin1a2lem11  8052  dcomex  8089  ttukeylem1  8152  ttukeylem7  8158  ondomon  8201  konigthlem  8206  alephadd  8215  alephexp1  8217  alephreg  8220  pwcfsdom  8221  fpwwe2lem13  8280  gchaleph  8313  gchaleph2  8314  winainflem  8331  inttsk  8412  inar1  8413  inatsk  8416  grudomon  8455  nqerid  8573  nqpr  8654  zmin  10328  uzrdgsuci  11039  limsupval2  11970  caucvgb  12168  sumz  12211  fsumsers  12217  isumclim  12236  isumnn0nn  12317  climcndslem1  12324  climcndslem2  12325  alzdvds  12594  bitsfzolem  12641  phicl2  12852  phibnd  12855  pclem  12907  strle1  13255  psss  14339  dprdss  15280  2ndcdisj  17198  dis2ndc  17202  hausmapdom  17242  ptcnplem  17331  fbun  17551  metrest  18086  opnreen  18352  bndth  18472  cmetcaulem  18730  ivthle  18832  ivthle2  18833  ovolfiniun  18876  volfiniun  18920  uniiccdif  18949  uniioovol  18950  uniioombllem4  18957  dyadmbl  18971  vitali  18984  mbfdm  18999  mbflimsup  19037  itg2monolem2  19122  itg2monolem3  19123  itg2mono  19124  cpnres  19302  dvcj  19315  dvef  19343  dvne0  19374  lhop2  19378  itgparts  19410  itgsubstlem  19411  ply1divex  19538  fta1blem  19570  dgrlem  19627  pige3  19901  xrlimcnp  20279  ftalem3  20328  lgsdchr  20603  dchrvmasumlem2  20663  pntlem3  20774  chscllem4  22235  adjeq  22531  hmopidmchi  22747  ballotlemfc0  23067  ballotlemfcc  23068  xreceu  23121  measvuni  23557  iccllyscon  23796  cvmliftphtlem  23863  umgraex  23890  zprodn0  24162  axcontlem2  24665  re1ax2lem  24893  re1ax2  24894  cbcpcp  25265  int2pre  25340  intopcoaconlem3  25642  limptlimpr2lem2  25678  islimrs4  25685  altretop  25703  cnegvex2  25763  rnegvex2  25764  hdrmp  25809  prismorcsetlemc  26020  iscol3  26197  opnrebl2  26339  totbndbnd  26616  rabdiophlem1  26985  pellexlem5  27021  ttac  27232  aomclem4  27257  hbtlem5  27435  idomodle  27615  idomsubgmo  27617  ndmaovcl  28171  vk15.4j  28590  a9e2nd  28623  ee01OLD  28769  trsspwALT2  28909  sspwtrALT  28912  sstrALT2  28927  a16gNEW7  29521  islsati  29806  hdmap14lem2a  32682
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator