Theorem mpsyl 68

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

Step	Hyp	Ref	Expression
1		mpsyl.1	. . 3 |- ph
2	1	a1i 11	. 2 |- ( ps -> ph )
3		mpsyl.2	. 2 |- ( ps -> ch )
4		mpsyl.3	. 2 |- ( ph -> ( ch -> th ) )
5	2, 3, 4	sylc 65	1 |- ( ps -> th )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  tbwlem1  1630  tbwlem2  1631  re1luk3  1637  merco1lem17  1658  re1tbw1  1670  relcnvtr  5655  relresfld  5662  onfr  5763  foimacnv  6154  fvi  6255  isoini2  6589  ovidig  6778  f1oexbi  7116  frxp  7287  smores2  7451  tfrlem5  7476  mapdom1  8125  php2  8145  snnen2o  8149  frfi  8205  fodomfi  8239  ixpfi2  8264  hartogs  8449  wemapsolem  8455  card2on  8459  unwdomg  8489  r1pwss  8647  tz9.12lem3  8652  uniwf  8682  rankval3b  8689  tskwe  8776  carddomi2  8796  cardsdomelir  8799  infxpenlem  8836  inffien  8886  alephord  8898  alephdom  8904  iunfictbso  8937  dfac8  8957  dfacacn  8963  dfac13  8964  dfac12lem2  8966  infmap2  9040  ackbij1b  9061  ackbij2  9065  fictb  9067  cfslb  9088  fin67  9217  fin1a2lem10  9231  fin1a2lem11  9232  dcomex  9269  ttukeylem1  9331  ttukeylem7  9337  ondomon  9385  konigthlem  9390  alephadd  9399  alephexp1  9401  alephreg  9404  pwcfsdom  9405  fpwwe2lem13  9464  gchaleph  9493  gchaleph2  9494  winainflem  9515  inttsk  9596  inar1  9597  inatsk  9600  grudomon  9639  nqerid  9755  nqpr  9836  zmin  11784  uzrdgsuci  12759  isfinite4  13153  swrdccatin12lem3  13490  limsupval2  14211  caucvgb  14410  sumz  14453  fsumsers  14459  isumclim  14488  isumnn0nn  14574  climcndslem1  14581  climcndslem2  14582  ntrivcvgfvn0  14631  ntrivcvgtail  14632  zprodn0  14669  iprodclim  14729  alzdvds  15042  bitsfzolem  15156  phicl2  15473  phibnd  15476  pclem  15543  strle1  15973  psss  17214  symg2bas  17818  dprdss  18428  2ndcdisj  21259  dis2ndc  21263  hausmapdom  21303  ptcnplem  21424  fbun  21644  metrest  22329  opnreen  22634  bndth  22757  cmetcaulem  23086  ivthle  23225  ivthle2  23226  ovolfiniun  23269  volfiniun  23315  uniiccdif  23346  uniioovol  23347  uniioombllem4  23354  dyadmbl  23368  vitali  23382  mbfdm  23395  mbflimsup  23433  itg2monolem2  23518  itg2monolem3  23519  itg2mono  23520  cpnres  23700  dvcj  23713  dvef  23743  dvne0  23774  lhop2  23778  itgparts  23810  itgsubstlem  23811  ply1divex  23896  fta1blem  23928  dgrlem  23985  pige3  24269  xrlimcnp  24695  lgambdd  24763  ftalem3  24801  lgsdchr  25080  2lgslem1  25119  dchrvmasumlem2  25187  pntlem3  25298  tgisline  25522  axcontlem2  25845  upgrex  25987  umgrnloop2  26041  usgriedgleord  26120  uspgredgleord  26124  nbedgusgr  26274  rusgrnumwrdl2  26482  wlkp1lem2  26571  wlknwwlksnbij2  26778  wlkwwlkbij2  26785  wwlksnexthasheq  26798  wlksnwwlknvbij  26803  2pthon3v  26839  umgr2wlk  26845  rusgrnumwlkg  26872  umgrclwwlksge2  26912  clwwlksbij  26920  clwwlksvbij  26922  0pthonv  26990  1pthon2v  27013  numclwlk1lem2  27230  numclwwlk1  27231  numclwwlkqhash  27233  chscllem4  28499  adjeq  28794  hmopidmchi  29010  xreceu  29630  archirngz  29743  archiabllem1b  29746  locfinreflem  29907  measvuni  30277  elmbfmvol2  30329  omsmeas  30385  sibfof  30402  eulerpartlemgvv  30438  ballotlemfc0  30554  ballotlemfcc  30555  iccllysconn  31232  cvmliftphtlem  31299  opnrebl2  32316  re1ax2lem  32382  re1ax2  32383  bj-orim2  32541  bj-currypeirce  32544  bj-peircecurry  32545  lindsdom  33403  poimir  33442  volsupnfl  33454  areacirc  33505  totbndbnd  33588  islsati  34281  hdmap14lem2a  37159  rabdiophlem1  37365  pellexlem5  37397  ttac  37603  aomclem4  37627  hbtlem5  37698  idomodle  37774  idomsubgmo  37776  rp-isfinite5  37863  vk15.4j  38734  ax6e2nd  38774  eel0001  38945  trsspwALT2  39046  sspwtrALT  39049  sstrALT2  39070  dvmptconst  40129  dvmptidg  40131  fperdvper  40133  dvmulcncf  40140  dvdivcncf  40142  fourierdlem20  40344  fouriercn  40449  ndmaovcl  41283  fmtnofac2  41481  prminf2  41500  irinitoringc  42069  pgrpgt2nabl  42147  spcdvw  42426  aacllem  42547