Theorem mpsyl 68

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 65	1 ⊢ (𝜓 → 𝜃)

Syntax hints:   → wi 4

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

This theorem is referenced by:  spimew  1973  snssg  4742  relcnvtrg  6233  relresfld  6242  onfr  6364  foimacnv  6799  fvi  6918  isoini2  7295  ovidig  7510  f1oexbi  7880  frxp  8078  smores2  8296  tfrlem5  8321  en2sn  8990  en2prd  8996  mapdom1  9082  frfi  9197  fodomfi  9224  fodomfiOLD  9242  ixpfi2  9262  hartogs  9461  wemapsolem  9467  card2on  9471  unwdomg  9501  ttrclss  9641  r1pwss  9708  tz9.12lem3  9713  uniwf  9743  rankval3b  9750  djuun  9850  tskwe  9874  carddomi2  9894  cardsdomelir  9897  infxpenlem  9935  inffien  9985  alephord  9997  alephdom  10003  iunfictbso  10036  dfac8  10058  dfacacn  10064  dfac13  10065  dfac12lem2  10067  infmap2  10139  ackbij1b  10160  ackbij2  10164  fictb  10166  cfslb  10188  fin67  10317  fin1a2lem10  10331  fin1a2lem11  10332  dcomex  10369  ttukeylem1  10431  ttukeylem7  10437  ondomon  10485  konigthlem  10491  alephadd  10500  alephexp1  10502  alephreg  10505  pwcfsdom  10506  fpwwe2lem12  10565  gchaleph  10594  gchaleph2  10595  winainflem  10616  inttsk  10697  inar1  10698  inatsk  10701  grudomon  10740  nqerid  10856  nqpr  10937  zmin  12869  uzrdgsuci  13895  isfinite4  14297  pfxccatin12lem3  14667  limsupval2  15415  sumz  15657  fsumsers  15663  isumclim  15692  ntrivcvgfvn0  15834  ntrivcvgtail  15835  zprodn0  15874  iprodclim  15933  alzdvds  16259  bitsfzolem  16373  phicl2  16707  phibnd  16710  pclem  16778  strle1  17097  fnpr2ob  17491  psss  18515  symg2bas  19334  dprdss  19972  irinitoringc  21446  2ndcdisj  23412  dis2ndc  23416  hausmapdom  23456  ptcnplem  23577  fbun  23796  metrest  24480  opnreen  24788  ivthle  25425  ivthle2  25426  ovolfiniun  25470  volfiniun  25516  uniiccdif  25547  uniioovol  25548  uniioombllem4  25555  dyadmbl  25569  vitali  25582  mbflimsup  25635  cpnres  25907  dvcj  25922  dvef  25952  dvne0  25984  lhop2  25988  itgparts  26022  itgsubstlem  26023  ply1divex  26110  fta1blem  26144  dgrlem  26202  pige3ALT  26497  xrlimcnp  26946  ftalem3  27053  lgsdchr  27334  2lgslem1  27373  addsqn2reu  27420  2sqreultblem  27427  2sqreunnltblem  27430  dchrvmasumlem2  27477  pntlem3  27588  mulsproplem13  28136  mulsproplem14  28137  tgisline  28711  axcontlem2  29050  upgrex  29177  umgrnloop2  29231  usgriedgleord  29313  uspgredgleord  29317  nbedgusgr  29457  nb3grprlem2  29466  rusgrnumwrdl2  29672  wlkp1lem2  29758  wwlksnexthasheq  29988  wlksnwwlknvbij  29993  2pthon3v  30028  umgr2wlk  30034  rusgrnumwlkg  30065  umgrclwwlkge2  30078  clwwlkvbij  30200  0pthonv  30216  1pthon2v  30240  numclwwlkqhash  30462  chscllem4  31727  adjeq  32022  hmopidmchi  32238  xreceu  33013  tocyccntz  33237  archirngz  33282  archiabllem1b  33285  locfinreflem  34017  measvuni  34391  elmbfmvol2  34444  omsmeas  34500  sibfof  34517  eulerpartlemgvv  34553  ballotlemfc0  34670  ballotlemfcc  34671  rankval4b  35275  iccllysconn  35463  cvmliftphtlem  35530  satfv1  35576  sat1el2xp  35592  opnrebl2  36534  re1ax2lem  36600  re1ax2  36601  regsfromregtr  36687  bj-orim2  36777  bj-peircecurry  36779  lindsdom  37859  poimir  37898  volsupnfl  37910  areacirc  37958  totbndbnd  38034  islsati  39364  hdmap14lem2a  42237  rabdiophlem1  43152  pellexlem5  43184  ttac  43387  aomclem4  43408  hbtlem5  43479  idomodle  43542  idomsubgmo  43544  nnoeomeqom  43663  omabs2  43683  rp-isfinite5  43867  iscard4  43883  mnuunid  44627  vk15.4j  44878  ax6e2nd  44908  trsspwALT2  45168  sspwtrALT  45171  sstrALT2  45184  permaxrep  45356  dvmptconst  46267  dvmptidg  46269  fperdvper  46271  dvmulcncf  46277  dvdivcncf  46279  fourierdlem20  46479  fouriercn  46584  ndmaovcl  47557  fundcmpsurinjpreimafv  47762  fmtnofac2  47923  prminf2  47942  gpg5nbgrvtx03starlem1  48422  gpg5nbgrvtx03starlem2  48423  gpg5nbgrvtx03starlem3  48424  gpg5nbgrvtx13starlem1  48425  gpg5nbgrvtx13starlem2  48426  gpg5nbgrvtx13starlem3  48427  gpgprismgr4cyclex  48461  gpg5edgnedg  48484  pgrpgt2nabl  48720  line2x  49108  prstchom2ALT  49917  spcdvw  50032  aacllem  50154