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  1885  relcnvtr  5192  relresfld  5199  relcoi1  5201  foimacnv  5490  fvi  5579  isoini2  5836  ovidig  5965  frxp  6225  smores2  6371  mapdom1  7026  php2  7046  frfi  7102  fodomfi  7135  ixpfi2  7154  hartogs  7259  wemapso2lem  7265  card2on  7268  unwdomg  7298  r1pwss  7456  tz9.12lem3  7461  uniwf  7491  rankval3b  7498  tskwe  7583  carddomi2  7603  cardsdomelir  7606  infxpenlem  7641  inffien  7690  alephord  7702  alephdom  7708  iunfictbso  7741  dfac8  7761  dfacacn  7767  dfac13  7768  dfac12lem2  7770  infmap2  7844  ackbij1b  7865  ackbij2  7869  fictb  7871  cfslb  7892  fin67  8021  fin1a2lem10  8035  fin1a2lem11  8036  dcomex  8073  ttukeylem1  8136  ttukeylem7  8142  ondomon  8185  konigthlem  8190  alephadd  8199  alephexp1  8201  alephreg  8204  pwcfsdom  8205  fpwwe2lem13  8264  gchaleph  8297  gchaleph2  8298  winainflem  8315  inttsk  8396  inar1  8397  inatsk  8400  grudomon  8439  nqerid  8557  nqpr  8638  zmin  10312  uzrdgsuci  11023  limsupval2  11954  caucvgb  12152  sumz  12195  fsumsers  12201  isumclim  12220  isumnn0nn  12301  climcndslem1  12308  climcndslem2  12309  alzdvds  12578  bitsfzolem  12625  phicl2  12836  phibnd  12839  pclem  12891  strle1  13239  psss  14323  dprdss  15264  2ndcdisj  17182  dis2ndc  17186  hausmapdom  17226  ptcnplem  17315  fbun  17535  metrest  18070  opnreen  18336  bndth  18456  cmetcaulem  18714  ivthle  18816  ivthle2  18817  ovolfiniun  18860  volfiniun  18904  uniiccdif  18933  uniioovol  18934  uniioombllem4  18941  dyadmbl  18955  vitali  18968  mbfdm  18983  mbflimsup  19021  itg2monolem2  19106  itg2monolem3  19107  itg2mono  19108  cpnres  19286  dvcj  19299  dvef  19327  dvne0  19358  lhop2  19362  itgparts  19394  itgsubstlem  19395  ply1divex  19522  fta1blem  19554  dgrlem  19611  pige3  19885  xrlimcnp  20263  ftalem3  20312  lgsdchr  20587  dchrvmasumlem2  20647  pntlem3  20758  chscllem4  22219  adjeq  22515  hmopidmchi  22731  ballotlemfc0  23051  ballotlemfcc  23052  xreceu  23105  measvuni  23542  iccllyscon  23781  cvmliftphtlem  23848  umgraex  23875  axcontlem2  24593  re1ax2lem  24821  re1ax2  24822  cbcpcp  25162  int2pre  25237  intopcoaconlem3  25539  limptlimpr2lem2  25575  islimrs4  25582  altretop  25600  cnegvex2  25660  rnegvex2  25661  hdrmp  25706  prismorcsetlemc  25917  iscol3  26094  opnrebl2  26236  totbndbnd  26513  rabdiophlem1  26882  pellexlem5  26918  ttac  27129  aomclem4  27154  hbtlem5  27332  idomodle  27512  idomsubgmo  27514  ndmaovcl  28063  vk15.4j  28291  a9e2nd  28324  ee01OLD  28464  trsspwALT2  28593  sspwtrALT  28596  sstrALT2  28611  islsati  29184  hdmap14lem2a  32060
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator