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  1990  snssg  4741  relcnvtrg  6250  relresfld  6259  onfr  6381  foimacnv  6820  fvi  6939  isoini2  7319  ovidig  7534  f1oexbi  7905  frxp  8101  smores2  8320  tfrlem5  8345  en2sn  9018  en2prd  9024  mapdom1  9110  frfi  9225  fodomfi  9252  fodomfiOLD  9270  ixpfi2  9290  hartogs  9489  wemapsolem  9495  card2on  9499  unwdomg  9529  ttrclss  9672  r1pwss  9739  tz9.12lem3  9744  uniwf  9774  rankval3b  9781  djuun  9881  tskwe  9905  carddomi2  9925  cardsdomelir  9928  infxpenlem  9966  inffien  10016  alephord  10028  alephdom  10034  iunfictbso  10067  dfac8  10089  dfacacn  10095  dfac13  10096  dfac12lem2  10098  infmap2  10170  ackbij1b  10191  ackbij2  10195  fictb  10197  cfslb  10220  fin67  10349  fin1a2lem10  10363  fin1a2lem11  10364  dcomex  10401  ttukeylem1  10463  ttukeylem7  10469  ondomon  10517  konigthlem  10523  alephadd  10532  alephexp1  10534  alephreg  10537  pwcfsdom  10538  fpwwe2lem12  10597  gchaleph  10626  gchaleph2  10627  winainflem  10648  inttsk  10729  inar1  10730  inatsk  10733  grudomon  10772  nqerid  10888  nqpr  10969  zmin  12942  uzrdgsuci  13970  isfinite4  14372  pfxccatin12lem3  14742  limsupval2  15490  sumz  15732  fsumsers  15738  isumclim  15767  ntrivcvgfvn0  15912  ntrivcvgtail  15913  zprodn0  15952  iprodclim  16011  alzdvds  16337  bitsfzolem  16451  phicl2  16786  phibnd  16789  pclem  16857  strle1  17177  fnpr2ob  17571  psss  18595  symg2bas  19416  dprdss  20054  irinitoringc  21511  2ndcdisj  23496  dis2ndc  23500  hausmapdom  23540  ptcnplem  23661  fbun  23880  metrest  24564  opnreen  24872  ivthle  25498  ivthle2  25499  ovolfiniun  25543  volfiniun  25589  uniiccdif  25620  uniioovol  25621  uniioombllem4  25628  dyadmbl  25642  vitali  25655  mbflimsup  25708  cpnres  25979  dvcj  25992  dvef  26022  dvne0  26053  lhop2  26057  itgparts  26089  itgsubstlem  26090  ply1divex  26177  fta1blem  26211  dgrlem  26269  pige3ALT  26562  xrlimcnp  27010  ftalem3  27116  lgsdchr  27396  2lgslem1  27435  addsqn2reu  27482  2sqreultblem  27489  2sqreunnltblem  27492  dchrvmasumlem2  27539  pntlem3  27650  mulsproplem13  28198  mulsproplem14  28199  tgisline  28773  axcontlem2  29112  upgrex  29239  umgrnloop2  29293  usgriedgleord  29375  uspgredgleord  29379  nbedgusgr  29519  nb3grprlem2  29528  rusgrnumwrdl2  29733  wlkp1lem2  29819  wwlksnexthasheq  30049  wlksnwwlknvbij  30054  2pthon3v  30089  umgr2wlk  30095  rusgrnumwlkg  30126  umgrclwwlkge2  30139  clwwlkvbij  30261  0pthonv  30277  1pthon2v  30301  numclwwlkqhash  30523  chscllem4  31789  adjeq  32084  hmopidmchi  32300  xreceu  33060  tocyccntz  33285  archirngz  33330  archiabllem1b  33333  locfinreflem  34098  measvuni  34472  elmbfmvol2  34525  omsmeas  34581  sibfof  34598  eulerpartlemgvv  34634  ballotlemfc0  34751  ballotlemfcc  34752  rankval4b  35360  iccllysconn  35564  cvmliftphtlem  35631  satfv1  35677  sat1el2xp  35693  opnrebl2  36645  re1ax2lem  36711  re1ax2  36712  regsfromregtco  36862  bj-orim2  36962  bj-peircecurry  36964  lindsdom  38077  poimir  38116  volsupnfl  38128  areacirc  38176  totbndbnd  38252  islsati  39582  hdmap14lem2a  42455  rabdiophlem1  43342  pellexlem5  43374  ttac  43577  aomclem4  43598  hbtlem5  43669  idomodle  43732  idomsubgmo  43734  nnoeomeqom  43853  omabs2  43873  rp-isfinite5  44057  iscard4  44073  mnuunid  44817  vk15.4j  45068  ax6e2nd  45098  trsspwALT2  45358  sspwtrALT  45361  sstrALT2  45374  permaxrep  45546  dvmptconst  46453  dvmptidg  46455  fperdvper  46457  dvmulcncf  46463  dvdivcncf  46465  fourierdlem20  46665  fouriercn  46770  ndmaovcl  47761  fundcmpsurinjpreimafv  47978  fmtnofac2  48142  prminf2  48161  gpg5nbgrvtx03starlem1  48654  gpg5nbgrvtx03starlem2  48655  gpg5nbgrvtx03starlem3  48656  gpg5nbgrvtx13starlem1  48657  gpg5nbgrvtx13starlem2  48658  gpg5nbgrvtx13starlem3  48659  gpgprismgr4cyclex  48693  gpg5edgnedg  48716  pgrpgt2nabl  48952  line2x  49340  prstchom2ALT  50149  spcdvw  50264  aacllem  50386