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  1970  snssg  4756  relcnvtrg  6252  relresfld  6262  onfr  6388  foimacnv  6831  fvi  6951  isoini2  7327  ovidig  7543  f1oexbi  7918  frxp  8119  smores2  8362  tfrlem5  8388  en2sn  9049  en2prd  9056  mapdom1  9150  php2OLD  9226  snnen2oOLD  9230  frfi  9287  fodomfi  9316  fodomfiOLD  9336  ixpfi2  9356  hartogs  9550  wemapsolem  9556  card2on  9560  unwdomg  9590  ttrclss  9726  r1pwss  9790  tz9.12lem3  9795  uniwf  9825  rankval3b  9832  djuun  9932  tskwe  9956  carddomi2  9976  cardsdomelir  9979  infxpenlem  10019  inffien  10069  alephord  10081  alephdom  10087  iunfictbso  10120  dfac8  10142  dfacacn  10148  dfac13  10149  dfac12lem2  10151  infmap2  10223  ackbij1b  10244  ackbij2  10248  fictb  10250  cfslb  10272  fin67  10401  fin1a2lem10  10415  fin1a2lem11  10416  dcomex  10453  ttukeylem1  10515  ttukeylem7  10521  ondomon  10569  konigthlem  10574  alephadd  10583  alephexp1  10585  alephreg  10588  pwcfsdom  10589  fpwwe2lem12  10648  gchaleph  10677  gchaleph2  10678  winainflem  10699  inttsk  10780  inar1  10781  inatsk  10784  grudomon  10823  nqerid  10939  nqpr  11020  zmin  12952  uzrdgsuci  13967  isfinite4  14368  pfxccatin12lem3  14737  limsupval2  15483  sumz  15725  fsumsers  15731  isumclim  15760  ntrivcvgfvn0  15902  ntrivcvgtail  15903  zprodn0  15942  iprodclim  16001  alzdvds  16324  bitsfzolem  16438  phicl2  16772  phibnd  16775  pclem  16843  strle1  17162  fnpr2ob  17557  psss  18575  symg2bas  19359  dprdss  19997  irinitoringc  21425  2ndcdisj  23379  dis2ndc  23383  hausmapdom  23423  ptcnplem  23544  fbun  23763  metrest  24448  opnreen  24756  ivthle  25394  ivthle2  25395  ovolfiniun  25439  volfiniun  25485  uniiccdif  25516  uniioovol  25517  uniioombllem4  25524  dyadmbl  25538  vitali  25551  mbflimsup  25604  cpnres  25876  dvcj  25891  dvef  25921  dvne0  25953  lhop2  25957  itgparts  25991  itgsubstlem  25992  ply1divex  26079  fta1blem  26113  dgrlem  26171  pige3ALT  26465  xrlimcnp  26914  ftalem3  27021  lgsdchr  27302  2lgslem1  27341  addsqn2reu  27388  2sqreultblem  27395  2sqreunnltblem  27398  dchrvmasumlem2  27445  pntlem3  27556  mulsproplem13  28057  mulsproplem14  28058  tgisline  28538  axcontlem2  28876  upgrex  29003  umgrnloop2  29057  usgriedgleord  29139  uspgredgleord  29143  nbedgusgr  29283  nb3grprlem2  29292  rusgrnumwrdl2  29498  wlkp1lem2  29586  wwlksnexthasheq  29817  wlksnwwlknvbij  29822  2pthon3v  29857  umgr2wlk  29863  rusgrnumwlkg  29891  umgrclwwlkge2  29904  clwwlkvbij  30026  0pthonv  30042  1pthon2v  30066  numclwwlkqhash  30288  chscllem4  31553  adjeq  31848  hmopidmchi  32064  xreceu  32814  tocyccntz  33073  archirngz  33105  archiabllem1b  33108  locfinreflem  33779  measvuni  34153  elmbfmvol2  34207  omsmeas  34263  sibfof  34280  eulerpartlemgvv  34316  ballotlemfc0  34433  ballotlemfcc  34434  iccllysconn  35193  cvmliftphtlem  35260  satfv1  35306  sat1el2xp  35322  opnrebl2  36260  re1ax2lem  36326  re1ax2  36327  bj-orim2  36495  bj-peircecurry  36497  lindsdom  37559  poimir  37598  volsupnfl  37610  areacirc  37658  totbndbnd  37734  islsati  38933  hdmap14lem2a  41807  rabdiophlem1  42749  pellexlem5  42781  ttac  42985  aomclem4  43006  hbtlem5  43077  idomodle  43140  idomsubgmo  43142  nnoeomeqom  43261  omabs2  43281  rp-isfinite5  43466  iscard4  43482  mnuunid  44227  vk15.4j  44479  ax6e2nd  44509  trsspwALT2  44770  sspwtrALT  44773  sstrALT2  44786  permaxrep  44958  dvmptconst  45874  dvmptidg  45876  fperdvper  45878  dvmulcncf  45884  dvdivcncf  45886  fourierdlem20  46086  fouriercn  46191  ndmaovcl  47160  fundcmpsurinjpreimafv  47340  fmtnofac2  47501  prminf2  47520  gpg5nbgrvtx03starlem1  47969  gpg5nbgrvtx03starlem2  47970  gpg5nbgrvtx03starlem3  47971  gpg5nbgrvtx13starlem1  47972  gpg5nbgrvtx13starlem2  47973  gpg5nbgrvtx13starlem3  47974  pgrpgt2nabl  48227  line2x  48620  prstchom2ALT  49226  spcdvw  49263  aacllem  49385