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  1972  snssg  4740  relcnvtrg  6225  relresfld  6234  onfr  6356  foimacnv  6791  fvi  6910  isoini2  7285  ovidig  7500  f1oexbi  7870  frxp  8068  smores2  8286  tfrlem5  8311  en2sn  8978  en2prd  8984  mapdom1  9070  frfi  9185  fodomfi  9212  fodomfiOLD  9230  ixpfi2  9250  hartogs  9449  wemapsolem  9455  card2on  9459  unwdomg  9489  ttrclss  9629  r1pwss  9696  tz9.12lem3  9701  uniwf  9731  rankval3b  9738  djuun  9838  tskwe  9862  carddomi2  9882  cardsdomelir  9885  infxpenlem  9923  inffien  9973  alephord  9985  alephdom  9991  iunfictbso  10024  dfac8  10046  dfacacn  10052  dfac13  10053  dfac12lem2  10055  infmap2  10127  ackbij1b  10148  ackbij2  10152  fictb  10154  cfslb  10176  fin67  10305  fin1a2lem10  10319  fin1a2lem11  10320  dcomex  10357  ttukeylem1  10419  ttukeylem7  10425  ondomon  10473  konigthlem  10479  alephadd  10488  alephexp1  10490  alephreg  10493  pwcfsdom  10494  fpwwe2lem12  10553  gchaleph  10582  gchaleph2  10583  winainflem  10604  inttsk  10685  inar1  10686  inatsk  10689  grudomon  10728  nqerid  10844  nqpr  10925  zmin  12857  uzrdgsuci  13883  isfinite4  14285  pfxccatin12lem3  14655  limsupval2  15403  sumz  15645  fsumsers  15651  isumclim  15680  ntrivcvgfvn0  15822  ntrivcvgtail  15823  zprodn0  15862  iprodclim  15921  alzdvds  16247  bitsfzolem  16361  phicl2  16695  phibnd  16698  pclem  16766  strle1  17085  fnpr2ob  17479  psss  18503  symg2bas  19322  dprdss  19960  irinitoringc  21434  2ndcdisj  23400  dis2ndc  23404  hausmapdom  23444  ptcnplem  23565  fbun  23784  metrest  24468  opnreen  24776  ivthle  25413  ivthle2  25414  ovolfiniun  25458  volfiniun  25504  uniiccdif  25535  uniioovol  25536  uniioombllem4  25543  dyadmbl  25557  vitali  25570  mbflimsup  25623  cpnres  25895  dvcj  25910  dvef  25940  dvne0  25972  lhop2  25976  itgparts  26010  itgsubstlem  26011  ply1divex  26098  fta1blem  26132  dgrlem  26190  pige3ALT  26485  xrlimcnp  26934  ftalem3  27041  lgsdchr  27322  2lgslem1  27361  addsqn2reu  27408  2sqreultblem  27415  2sqreunnltblem  27418  dchrvmasumlem2  27465  pntlem3  27576  mulsproplem13  28124  mulsproplem14  28125  tgisline  28699  axcontlem2  29038  upgrex  29165  umgrnloop2  29219  usgriedgleord  29301  uspgredgleord  29305  nbedgusgr  29445  nb3grprlem2  29454  rusgrnumwrdl2  29660  wlkp1lem2  29746  wwlksnexthasheq  29976  wlksnwwlknvbij  29981  2pthon3v  30016  umgr2wlk  30022  rusgrnumwlkg  30053  umgrclwwlkge2  30066  clwwlkvbij  30188  0pthonv  30204  1pthon2v  30228  numclwwlkqhash  30450  chscllem4  31715  adjeq  32010  hmopidmchi  32226  xreceu  33003  tocyccntz  33226  archirngz  33271  archiabllem1b  33274  locfinreflem  33997  measvuni  34371  elmbfmvol2  34424  omsmeas  34480  sibfof  34497  eulerpartlemgvv  34533  ballotlemfc0  34650  ballotlemfcc  34651  rankval4b  35256  iccllysconn  35444  cvmliftphtlem  35511  satfv1  35557  sat1el2xp  35573  opnrebl2  36515  re1ax2lem  36581  re1ax2  36582  regsfromregtr  36668  bj-orim2  36756  bj-peircecurry  36758  lindsdom  37811  poimir  37850  volsupnfl  37862  areacirc  37910  totbndbnd  37986  islsati  39250  hdmap14lem2a  42123  rabdiophlem1  43039  pellexlem5  43071  ttac  43274  aomclem4  43295  hbtlem5  43366  idomodle  43429  idomsubgmo  43431  nnoeomeqom  43550  omabs2  43570  rp-isfinite5  43754  iscard4  43770  mnuunid  44514  vk15.4j  44765  ax6e2nd  44795  trsspwALT2  45055  sspwtrALT  45058  sstrALT2  45071  permaxrep  45243  dvmptconst  46155  dvmptidg  46157  fperdvper  46159  dvmulcncf  46165  dvdivcncf  46167  fourierdlem20  46367  fouriercn  46472  ndmaovcl  47445  fundcmpsurinjpreimafv  47650  fmtnofac2  47811  prminf2  47830  gpg5nbgrvtx03starlem1  48310  gpg5nbgrvtx03starlem2  48311  gpg5nbgrvtx03starlem3  48312  gpg5nbgrvtx13starlem1  48313  gpg5nbgrvtx13starlem2  48314  gpg5nbgrvtx13starlem3  48315  gpgprismgr4cyclex  48349  gpg5edgnedg  48372  pgrpgt2nabl  48608  line2x  48996  prstchom2ALT  49805  spcdvw  49920  aacllem  50042