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  1971  snssg  4759  relcnvtrg  6255  relresfld  6265  onfr  6391  foimacnv  6834  fvi  6954  isoini2  7331  ovidig  7547  f1oexbi  7922  frxp  8123  smores2  8366  tfrlem5  8392  en2sn  9053  en2prd  9060  mapdom1  9154  php2OLD  9230  snnen2oOLD  9234  frfi  9291  fodomfi  9320  fodomfiOLD  9340  ixpfi2  9360  hartogs  9556  wemapsolem  9562  card2on  9566  unwdomg  9596  ttrclss  9732  r1pwss  9796  tz9.12lem3  9801  uniwf  9831  rankval3b  9838  djuun  9938  tskwe  9962  carddomi2  9982  cardsdomelir  9985  infxpenlem  10025  inffien  10075  alephord  10087  alephdom  10093  iunfictbso  10126  dfac8  10148  dfacacn  10154  dfac13  10155  dfac12lem2  10157  infmap2  10229  ackbij1b  10250  ackbij2  10254  fictb  10256  cfslb  10278  fin67  10407  fin1a2lem10  10421  fin1a2lem11  10422  dcomex  10459  ttukeylem1  10521  ttukeylem7  10527  ondomon  10575  konigthlem  10580  alephadd  10589  alephexp1  10591  alephreg  10594  pwcfsdom  10595  fpwwe2lem12  10654  gchaleph  10683  gchaleph2  10684  winainflem  10705  inttsk  10786  inar1  10787  inatsk  10790  grudomon  10829  nqerid  10945  nqpr  11026  zmin  12958  uzrdgsuci  13976  isfinite4  14378  pfxccatin12lem3  14748  limsupval2  15494  sumz  15736  fsumsers  15742  isumclim  15771  ntrivcvgfvn0  15913  ntrivcvgtail  15914  zprodn0  15953  iprodclim  16012  alzdvds  16337  bitsfzolem  16451  phicl2  16785  phibnd  16788  pclem  16856  strle1  17175  fnpr2ob  17570  psss  18588  symg2bas  19372  dprdss  20010  irinitoringc  21438  2ndcdisj  23392  dis2ndc  23396  hausmapdom  23436  ptcnplem  23557  fbun  23776  metrest  24461  opnreen  24769  ivthle  25407  ivthle2  25408  ovolfiniun  25452  volfiniun  25498  uniiccdif  25529  uniioovol  25530  uniioombllem4  25537  dyadmbl  25551  vitali  25564  mbflimsup  25617  cpnres  25889  dvcj  25904  dvef  25934  dvne0  25966  lhop2  25970  itgparts  26004  itgsubstlem  26005  ply1divex  26092  fta1blem  26126  dgrlem  26184  pige3ALT  26479  xrlimcnp  26928  ftalem3  27035  lgsdchr  27316  2lgslem1  27355  addsqn2reu  27402  2sqreultblem  27409  2sqreunnltblem  27412  dchrvmasumlem2  27459  pntlem3  27570  mulsproplem13  28071  mulsproplem14  28072  tgisline  28552  axcontlem2  28890  upgrex  29017  umgrnloop2  29071  usgriedgleord  29153  uspgredgleord  29157  nbedgusgr  29297  nb3grprlem2  29306  rusgrnumwrdl2  29512  wlkp1lem2  29600  wwlksnexthasheq  29831  wlksnwwlknvbij  29836  2pthon3v  29871  umgr2wlk  29877  rusgrnumwlkg  29905  umgrclwwlkge2  29918  clwwlkvbij  30040  0pthonv  30056  1pthon2v  30080  numclwwlkqhash  30302  chscllem4  31567  adjeq  31862  hmopidmchi  32078  xreceu  32842  tocyccntz  33101  archirngz  33133  archiabllem1b  33136  locfinreflem  33817  measvuni  34191  elmbfmvol2  34245  omsmeas  34301  sibfof  34318  eulerpartlemgvv  34354  ballotlemfc0  34471  ballotlemfcc  34472  iccllysconn  35218  cvmliftphtlem  35285  satfv1  35331  sat1el2xp  35347  opnrebl2  36285  re1ax2lem  36351  re1ax2  36352  bj-orim2  36520  bj-peircecurry  36522  lindsdom  37584  poimir  37623  volsupnfl  37635  areacirc  37683  totbndbnd  37759  islsati  38958  hdmap14lem2a  41832  rabdiophlem1  42771  pellexlem5  42803  ttac  43007  aomclem4  43028  hbtlem5  43099  idomodle  43162  idomsubgmo  43164  nnoeomeqom  43283  omabs2  43303  rp-isfinite5  43488  iscard4  43504  mnuunid  44249  vk15.4j  44501  ax6e2nd  44531  trsspwALT2  44791  sspwtrALT  44794  sstrALT2  44807  permaxrep  44979  dvmptconst  45892  dvmptidg  45894  fperdvper  45896  dvmulcncf  45902  dvdivcncf  45904  fourierdlem20  46104  fouriercn  46209  ndmaovcl  47180  fundcmpsurinjpreimafv  47370  fmtnofac2  47531  prminf2  47550  gpg5nbgrvtx03starlem1  48018  gpg5nbgrvtx03starlem2  48019  gpg5nbgrvtx03starlem3  48020  gpg5nbgrvtx13starlem1  48021  gpg5nbgrvtx13starlem2  48022  gpg5nbgrvtx13starlem3  48023  gpgprismgr4cyclex  48054  pgrpgt2nabl  48289  line2x  48682  prstchom2ALT  49389  spcdvw  49491  aacllem  49613