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:  tbwlem1  1708  tbwlem2  1709  re1luk3  1715  merco1lem17  1736  re1tbw1  1748  spimew  1976  relcnvtrg  6174  relresfld  6183  onfr  6309  foimacnv  6742  fvi  6853  isoini2  7219  ovidig  7424  f1oexbi  7784  frxp  7976  smores2  8194  tfrlem5  8220  en2sn  8840  en2snOLD  8841  mapdom1  8938  php2OLD  9015  snnen2oOLD  9019  frfi  9068  fodomfi  9101  ixpfi2  9126  hartogs  9312  wemapsolem  9318  card2on  9322  unwdomg  9352  ttrclss  9487  r1pwss  9551  tz9.12lem3  9556  uniwf  9586  rankval3b  9593  djuun  9693  tskwe  9717  carddomi2  9737  cardsdomelir  9740  infxpenlem  9778  inffien  9828  alephord  9840  alephdom  9846  iunfictbso  9879  dfac8  9900  dfacacn  9906  dfac13  9907  dfac12lem2  9909  infmap2  9983  ackbij1b  10004  ackbij2  10008  fictb  10010  cfslb  10031  fin67  10160  fin1a2lem10  10174  fin1a2lem11  10175  dcomex  10212  ttukeylem1  10274  ttukeylem7  10280  ondomon  10328  konigthlem  10333  alephadd  10342  alephexp1  10344  alephreg  10347  pwcfsdom  10348  fpwwe2lem12  10407  gchaleph  10436  gchaleph2  10437  winainflem  10458  inttsk  10539  inar1  10540  inatsk  10543  grudomon  10582  nqerid  10698  nqpr  10779  zmin  12693  uzrdgsuci  13689  isfinite4  14086  pfxccatin12lem3  14454  limsupval2  15198  sumz  15443  fsumsers  15449  isumclim  15478  ntrivcvgfvn0  15620  ntrivcvgtail  15621  zprodn0  15658  iprodclim  15717  alzdvds  16038  bitsfzolem  16150  phicl2  16478  phibnd  16481  pclem  16548  strle1  16868  fnpr2ob  17278  psss  18307  symg2bas  19009  dprdss  19641  2ndcdisj  22616  dis2ndc  22620  hausmapdom  22660  ptcnplem  22781  fbun  23000  metrest  23689  opnreen  24003  ivthle  24629  ivthle2  24630  ovolfiniun  24674  volfiniun  24720  uniiccdif  24751  uniioovol  24752  uniioombllem4  24759  dyadmbl  24773  vitali  24786  mbflimsup  24839  cpnres  25110  dvcj  25123  dvef  25153  dvne0  25184  lhop2  25188  itgparts  25220  itgsubstlem  25221  ply1divex  25310  fta1blem  25342  dgrlem  25399  pige3ALT  25685  xrlimcnp  26127  ftalem3  26233  lgsdchr  26512  2lgslem1  26551  addsqn2reu  26598  2sqreultblem  26605  2sqreunnltblem  26608  dchrvmasumlem2  26655  pntlem3  26766  tgisline  26997  axcontlem2  27342  upgrex  27471  umgrnloop2  27525  usgriedgleord  27604  uspgredgleord  27608  nbedgusgr  27748  nb3grprlem2  27757  rusgrnumwrdl2  27962  wlkp1lem2  28051  wwlksnexthasheq  28277  wlksnwwlknvbij  28282  2pthon3v  28317  umgr2wlk  28323  rusgrnumwlkg  28351  umgrclwwlkge2  28364  clwwlkvbij  28486  0pthonv  28502  1pthon2v  28526  numclwwlkqhash  28748  chscllem4  30011  adjeq  30306  hmopidmchi  30522  xreceu  31205  tocyccntz  31420  archirngz  31452  archiabllem1b  31455  locfinreflem  31799  measvuni  32191  elmbfmvol2  32243  omsmeas  32299  sibfof  32316  eulerpartlemgvv  32352  ballotlemfc0  32468  ballotlemfcc  32469  iccllysconn  33221  cvmliftphtlem  33288  satfv1  33334  sat1el2xp  33350  opnrebl2  34519  re1ax2lem  34585  re1ax2  34586  bj-orim2  34745  bj-peircecurry  34747  lindsdom  35780  poimir  35819  volsupnfl  35831  areacirc  35879  totbndbnd  35956  islsati  37015  hdmap14lem2a  39888  rabdiophlem1  40630  pellexlem5  40662  ttac  40865  aomclem4  40889  hbtlem5  40960  idomodle  41028  idomsubgmo  41030  rp-isfinite5  41131  iscard4  41147  mnuunid  41902  vk15.4j  42155  ax6e2nd  42185  trsspwALT2  42446  sspwtrALT  42449  sstrALT2  42462  dvmptconst  43463  dvmptidg  43465  fperdvper  43467  dvmulcncf  43473  dvdivcncf  43475  fourierdlem20  43675  fouriercn  43780  ndmaovcl  44706  fundcmpsurinjpreimafv  44871  fmtnofac2  45032  prminf2  45051  isomuspgrlem2  45296  irinitoringc  45638  pgrpgt2nabl  45713  line2x  46111  prstchom2ALT  46371  spcdvw  46396  aacllem  46516