Theorem mpsyl 63

Description: Modus ponens combined with a syllogism inference. (Contributed by Alan Sare, 20-Apr-2011.)

Hypotheses

Ref	Expression
mpsyl.1
mpsyl.2
mpsyl.3

Assertion

Ref	Expression
mpsyl

Proof of Theorem mpsyl

Step	Hyp	Ref	Expression
1		mpsyl.1	. . 3
2	1	a1i 11	. 2
3		mpsyl.2	. 2
4		mpsyl.3	. 2
5	2, 3, 4	sylc 60	1

Syntax hints:  ->wi 4

This theorem is referenced by:  tbwlem1  1538  tbwlem2  1539  re1luk3  1545  merco1lem17  1566  re1tbw1  1578  onfr  4922  relcnvtr  5532  relresfld  5539  relcoi1  5541  foimacnv  5838  fvi  5930  isoini2  6235  ovidig  6420  f1oexbi  6750  frxp  6910  smores2  7044  tfrlem5  7068  mapdom1  7702  php2  7722  snnen2o  7726  frfi  7785  fodomfi  7819  ixpfi2  7838  hartogs  7990  wemapsolem  7996  card2on  8001  unwdomg  8031  r1pwss  8223  tz9.12lem3  8228  uniwf  8258  rankval3b  8265  tskwe  8352  carddomi2  8372  cardsdomelir  8375  infxpenlem  8412  inffien  8465  alephord  8477  alephdom  8483  iunfictbso  8516  dfac8  8536  dfacacn  8542  dfac13  8543  dfac12lem2  8545  infmap2  8619  ackbij1b  8640  ackbij2  8644  fictb  8646  cfslb  8667  fin67  8796  fin1a2lem10  8810  fin1a2lem11  8811  dcomex  8848  ttukeylem1  8910  ttukeylem7  8916  ondomon  8959  konigthlem  8964  alephadd  8973  alephexp1  8975  alephreg  8978  pwcfsdom  8979  fpwwe2lem13  9041  gchaleph  9070  gchaleph2  9071  winainflem  9092  inttsk  9173  inar1  9174  inatsk  9177  grudomon  9216  nqerid  9332  nqpr  9413  zmin  11207  uzrdgsuci  12071  swrdccatin12lem3  12715  limsupval2  13303  caucvgb  13502  sumz  13544  fsumsers  13550  isumclim  13572  isumnn0nn  13654  climcndslem1  13661  climcndslem2  13662  ntrivcvgfvn0  13708  ntrivcvgtail  13709  zprodn0  13746  iprodclim  13791  alzdvds  14036  bitsfzolem  14084  phicl2  14298  phibnd  14301  pclem  14362  strle1  14728  psss  15844  symg2bas  16423  dprdss  17076  2ndcdisj  19957  dis2ndc  19961  hausmapdom  20001  ptcnplem  20122  fbun  20341  metrest  21027  opnreen  21336  bndth  21458  cmetcaulem  21727  ivthle  21868  ivthle2  21869  ovolfiniun  21912  volfiniun  21957  uniiccdif  21987  uniioovol  21988  uniioombllem4  21995  dyadmbl  22009  vitali  22022  mbfdm  22035  mbflimsup  22073  itg2monolem2  22158  itg2monolem3  22159  itg2mono  22160  cpnres  22340  dvcj  22353  dvef  22381  dvne0  22412  lhop2  22416  itgparts  22448  itgsubstlem  22449  ply1divex  22537  fta1blem  22569  dgrlem  22626  pige3  22910  xrlimcnp  23298  ftalem3  23348  lgsdchr  23623  dchrvmasumlem2  23683  pntlem3  23794  tgisline  24007  axcontlem2  24268  umgraex  24323  2trllemE  24555  0pthonv  24583  1pthon2v  24595  2pthon3v  24606  usg2wlk  24617  usg2wlkon  24618  wlknwwlknbij2  24714  wlkiswwlkbij2  24721  wlknwwlknvbij  24740  clwwlkgt0  24771  clwwlkbij  24799  clwwlkvbij  24801  rusgrasn  24945  numclwlk1lem2  25097  numclwwlk1  25098  numclwwlk2lem3  25106  chscllem4  26558  adjeq  26854  hmopidmchi  27070  xreceu  27618  archirngz  27733  archiabllem1b  27736  locfinreflem  27843  measvuni  28185  elmbfmvol2  28238  sibfof  28282  eulerpartlemgvv  28315  ballotlemfc0  28431  ballotlemfcc  28432  lgambdd  28579  iccllyscon  28695  cvmliftphtlem  28762  re1ax2lem  29848  re1ax2  29849  volsupnfl  30059  areacirc  30112  opnrebl2  30139  totbndbnd  30285  rabdiophlem1  30734  pellexlem5  30769  ttac  30978  aomclem4  31003  hbtlem5  31077  idomodle  31153  idomsubgmo  31155  dvmptconst  31710  dvmptidg  31712  fperdvper  31715  dvmulcncf  31722  dvdivcncf  31724  fourierdlem20  31909  fouriercn  32015  ndmaovcl  32288  usgedgleord  32419  usgedgleordALT  32420  usgo0fis  32438  usgo0fisALT  32439  irinitoringc  32877  pgrpgt2nabl  32959  aacllem  33216  vk15.4j  33298  ax6e2nd  33331  eel0001  33515  trsspwALT2  33617  sspwtrALT  33620  sstrALT2  33635  islsati  34719  hdmap14lem2a  37597  rp-isfinite4  37742  rp-isfinite5  37743

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