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  4737  relcnvtrg  6219  relresfld  6228  onfr  6350  foimacnv  6785  fvi  6903  isoini2  7280  ovidig  7495  f1oexbi  7868  frxp  8066  smores2  8284  tfrlem5  8309  en2sn  8973  en2prd  8980  mapdom1  9066  frfi  9190  fodomfi  9219  fodomfiOLD  9239  ixpfi2  9259  hartogs  9455  wemapsolem  9461  card2on  9465  unwdomg  9495  ttrclss  9635  r1pwss  9699  tz9.12lem3  9704  uniwf  9734  rankval3b  9741  djuun  9841  tskwe  9865  carddomi2  9885  cardsdomelir  9888  infxpenlem  9926  inffien  9976  alephord  9988  alephdom  9994  iunfictbso  10027  dfac8  10049  dfacacn  10055  dfac13  10056  dfac12lem2  10058  infmap2  10130  ackbij1b  10151  ackbij2  10155  fictb  10157  cfslb  10179  fin67  10308  fin1a2lem10  10322  fin1a2lem11  10323  dcomex  10360  ttukeylem1  10422  ttukeylem7  10428  ondomon  10476  konigthlem  10481  alephadd  10490  alephexp1  10492  alephreg  10495  pwcfsdom  10496  fpwwe2lem12  10555  gchaleph  10584  gchaleph2  10585  winainflem  10606  inttsk  10687  inar1  10688  inatsk  10691  grudomon  10730  nqerid  10846  nqpr  10927  zmin  12863  uzrdgsuci  13885  isfinite4  14287  pfxccatin12lem3  14656  limsupval2  15405  sumz  15647  fsumsers  15653  isumclim  15682  ntrivcvgfvn0  15824  ntrivcvgtail  15825  zprodn0  15864  iprodclim  15923  alzdvds  16249  bitsfzolem  16363  phicl2  16697  phibnd  16700  pclem  16768  strle1  17087  fnpr2ob  17480  psss  18504  symg2bas  19290  dprdss  19928  irinitoringc  21404  2ndcdisj  23359  dis2ndc  23363  hausmapdom  23403  ptcnplem  23524  fbun  23743  metrest  24428  opnreen  24736  ivthle  25373  ivthle2  25374  ovolfiniun  25418  volfiniun  25464  uniiccdif  25495  uniioovol  25496  uniioombllem4  25503  dyadmbl  25517  vitali  25530  mbflimsup  25583  cpnres  25855  dvcj  25870  dvef  25900  dvne0  25932  lhop2  25936  itgparts  25970  itgsubstlem  25971  ply1divex  26058  fta1blem  26092  dgrlem  26150  pige3ALT  26445  xrlimcnp  26894  ftalem3  27001  lgsdchr  27282  2lgslem1  27321  addsqn2reu  27368  2sqreultblem  27375  2sqreunnltblem  27378  dchrvmasumlem2  27425  pntlem3  27536  mulsproplem13  28054  mulsproplem14  28055  tgisline  28590  axcontlem2  28928  upgrex  29055  umgrnloop2  29109  usgriedgleord  29191  uspgredgleord  29195  nbedgusgr  29335  nb3grprlem2  29344  rusgrnumwrdl2  29550  wlkp1lem2  29636  wwlksnexthasheq  29866  wlksnwwlknvbij  29871  2pthon3v  29906  umgr2wlk  29912  rusgrnumwlkg  29940  umgrclwwlkge2  29953  clwwlkvbij  30075  0pthonv  30091  1pthon2v  30115  numclwwlkqhash  30337  chscllem4  31602  adjeq  31897  hmopidmchi  32113  xreceu  32875  tocyccntz  33099  archirngz  33141  archiabllem1b  33144  locfinreflem  33806  measvuni  34180  elmbfmvol2  34234  omsmeas  34290  sibfof  34307  eulerpartlemgvv  34343  ballotlemfc0  34460  ballotlemfcc  34461  iccllysconn  35222  cvmliftphtlem  35289  satfv1  35335  sat1el2xp  35351  opnrebl2  36294  re1ax2lem  36360  re1ax2  36361  bj-orim2  36529  bj-peircecurry  36531  lindsdom  37593  poimir  37632  volsupnfl  37644  areacirc  37692  totbndbnd  37768  islsati  38972  hdmap14lem2a  41846  rabdiophlem1  42774  pellexlem5  42806  ttac  43009  aomclem4  43030  hbtlem5  43101  idomodle  43164  idomsubgmo  43166  nnoeomeqom  43285  omabs2  43305  rp-isfinite5  43490  iscard4  43506  mnuunid  44250  vk15.4j  44502  ax6e2nd  44532  trsspwALT2  44792  sspwtrALT  44795  sstrALT2  44808  permaxrep  44980  dvmptconst  45897  dvmptidg  45899  fperdvper  45901  dvmulcncf  45907  dvdivcncf  45909  fourierdlem20  46109  fouriercn  46214  ndmaovcl  47188  fundcmpsurinjpreimafv  47393  fmtnofac2  47554  prminf2  47573  gpg5nbgrvtx03starlem1  48053  gpg5nbgrvtx03starlem2  48054  gpg5nbgrvtx03starlem3  48055  gpg5nbgrvtx13starlem1  48056  gpg5nbgrvtx13starlem2  48057  gpg5nbgrvtx13starlem3  48058  gpgprismgr4cyclex  48092  gpg5edgnedg  48115  pgrpgt2nabl  48351  line2x  48740  prstchom2ALT  49550  spcdvw  49665  aacllem  49787