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  1973  snssg  4728  relcnvtrg  6225  relresfld  6234  onfr  6356  foimacnv  6791  fvi  6910  isoini2  7287  ovidig  7502  f1oexbi  7872  frxp  8069  smores2  8287  tfrlem5  8312  en2sn  8981  en2prd  8987  mapdom1  9073  frfi  9188  fodomfi  9215  fodomfiOLD  9233  ixpfi2  9253  hartogs  9452  wemapsolem  9458  card2on  9462  unwdomg  9492  ttrclss  9632  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  10482  alephadd  10491  alephexp1  10493  alephreg  10496  pwcfsdom  10497  fpwwe2lem12  10556  gchaleph  10585  gchaleph2  10586  winainflem  10607  inttsk  10688  inar1  10689  inatsk  10692  grudomon  10731  nqerid  10847  nqpr  10928  zmin  12885  uzrdgsuci  13913  isfinite4  14315  pfxccatin12lem3  14685  limsupval2  15433  sumz  15675  fsumsers  15681  isumclim  15710  ntrivcvgfvn0  15855  ntrivcvgtail  15856  zprodn0  15895  iprodclim  15954  alzdvds  16280  bitsfzolem  16394  phicl2  16729  phibnd  16732  pclem  16800  strle1  17119  fnpr2ob  17513  psss  18537  symg2bas  19359  dprdss  19997  irinitoringc  21469  2ndcdisj  23431  dis2ndc  23435  hausmapdom  23475  ptcnplem  23596  fbun  23815  metrest  24499  opnreen  24807  ivthle  25433  ivthle2  25434  ovolfiniun  25478  volfiniun  25524  uniiccdif  25555  uniioovol  25556  uniioombllem4  25563  dyadmbl  25577  vitali  25590  mbflimsup  25643  cpnres  25914  dvcj  25927  dvef  25957  dvne0  25988  lhop2  25992  itgparts  26024  itgsubstlem  26025  ply1divex  26112  fta1blem  26146  dgrlem  26204  pige3ALT  26497  xrlimcnp  26945  ftalem3  27052  lgsdchr  27332  2lgslem1  27371  addsqn2reu  27418  2sqreultblem  27425  2sqreunnltblem  27428  dchrvmasumlem2  27475  pntlem3  27586  mulsproplem13  28134  mulsproplem14  28135  tgisline  28709  axcontlem2  29048  upgrex  29175  umgrnloop2  29229  usgriedgleord  29311  uspgredgleord  29315  nbedgusgr  29455  nb3grprlem2  29464  rusgrnumwrdl2  29670  wlkp1lem2  29756  wwlksnexthasheq  29986  wlksnwwlknvbij  29991  2pthon3v  30026  umgr2wlk  30032  rusgrnumwlkg  30063  umgrclwwlkge2  30076  clwwlkvbij  30198  0pthonv  30214  1pthon2v  30238  numclwwlkqhash  30460  chscllem4  31726  adjeq  32021  hmopidmchi  32237  xreceu  32996  tocyccntz  33220  archirngz  33265  archiabllem1b  33268  locfinreflem  34000  measvuni  34374  elmbfmvol2  34427  omsmeas  34483  sibfof  34500  eulerpartlemgvv  34536  ballotlemfc0  34653  ballotlemfcc  34654  rankval4b  35259  iccllysconn  35448  cvmliftphtlem  35515  satfv1  35561  sat1el2xp  35577  opnrebl2  36519  re1ax2lem  36585  re1ax2  36586  regsfromregtco  36736  bj-orim2  36836  bj-peircecurry  36838  lindsdom  37949  poimir  37988  volsupnfl  38000  areacirc  38048  totbndbnd  38124  islsati  39454  hdmap14lem2a  42327  rabdiophlem1  43247  pellexlem5  43279  ttac  43482  aomclem4  43503  hbtlem5  43574  idomodle  43637  idomsubgmo  43639  nnoeomeqom  43758  omabs2  43778  rp-isfinite5  43962  iscard4  43978  mnuunid  44722  vk15.4j  44973  ax6e2nd  45003  trsspwALT2  45263  sspwtrALT  45266  sstrALT2  45279  permaxrep  45451  dvmptconst  46361  dvmptidg  46363  fperdvper  46365  dvmulcncf  46371  dvdivcncf  46373  fourierdlem20  46573  fouriercn  46678  ndmaovcl  47663  fundcmpsurinjpreimafv  47880  fmtnofac2  48044  prminf2  48063  gpg5nbgrvtx03starlem1  48556  gpg5nbgrvtx03starlem2  48557  gpg5nbgrvtx03starlem3  48558  gpg5nbgrvtx13starlem1  48559  gpg5nbgrvtx13starlem2  48560  gpg5nbgrvtx13starlem3  48561  gpgprismgr4cyclex  48595  gpg5edgnedg  48618  pgrpgt2nabl  48854  line2x  49242  prstchom2ALT  50051  spcdvw  50166  aacllem  50288