Theorem mpsyl 69

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 66	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  1994  snssg  4745  relcnvtrg  6258  relresfld  6267  onfr  6389  foimacnv  6828  fvi  6947  isoini2  7327  ovidig  7542  f1oexbi  7913  frxp  8110  smores2  8329  tfrlem5  8354  en2sn  9026  en2prd  9032  mapdom1  9118  frfi  9233  fodomfi  9260  ixpfi2  9295  hartogs  9494  wemapsolem  9500  card2on  9504  unwdomg  9534  ttrclss  9677  r1pwss  9744  tz9.12lem3  9749  uniwf  9779  rankval3b  9786  djuun  9900  tskwe  9924  carddomi2  9944  cardsdomelir  9947  infxpenlem  9985  inffien  10035  alephord  10047  alephdom  10053  iunfictbso  10086  dfac8  10107  dfacacn  10113  dfac13  10114  dfac12lem2  10116  infmap2  10188  ackbij1b  10209  ackbij2  10213  fictb  10215  cfslb  10238  fin67  10367  fin1a2lem10  10381  fin1a2lem11  10382  dcomex  10419  ttukeylem1  10481  ttukeylem7  10487  ondomon  10535  konigthlem  10541  alephadd  10550  alephexp1  10552  alephreg  10555  pwcfsdom  10556  fpwwe2lem12  10615  gchaleph  10644  gchaleph2  10645  winainflem  10666  inttsk  10747  inar1  10748  inatsk  10751  grudomon  10790  nqerid  10906  nqpr  10987  zmin  12959  uzrdgsuci  13987  isfinite4  14389  pfxccatin12lem3  14759  limsupval2  15521  sumz  15763  fsumsers  15769  isumclim  15798  ntrivcvgfvn0  15943  ntrivcvgtail  15944  zprodn0  15983  iprodclim  16042  alzdvds  16368  bitsfzolem  16482  phicl2  16817  phibnd  16820  pclem  16888  strle1  17208  fnpr2ob  17602  psss  18626  symg2bas  19454  dprdss  20092  irinitoringc  21589  2ndcdisj  23574  dis2ndc  23578  hausmapdom  23618  ptcnplem  23739  fbun  23958  metrest  24642  opnreen  24950  ivthle  25576  ivthle2  25577  ovolfiniun  25621  volfiniun  25667  uniiccdif  25698  uniioovol  25699  uniioombllem4  25706  dyadmbl  25720  vitali  25733  mbflimsup  25786  cpnres  26057  dvcj  26070  dvef  26100  dvne0  26131  lhop2  26135  itgparts  26167  itgsubstlem  26168  ply1divex  26255  fta1blem  26289  dgrlem  26347  pige3ALT  26643  xrlimcnp  27091  ftalem3  27197  lgsdchr  27477  2lgslem1  27516  addsqn2reu  27563  2sqreultblem  27570  2sqreunnltblem  27573  dchrvmasumlem2  27620  pntlem3  27731  mulsproplem13  28279  mulsproplem14  28280  tgisline  28854  axcontlem2  29224  upgrex  29351  umgrnloop2  29405  usgriedgleord  29487  uspgredgleord  29491  nbedgusgr  29631  nb3grprlem2  29640  rusgrnumwrdl2  29845  wlkp1lem2  29931  wwlksnexthasheq  30161  wlksnwwlknvbij  30166  2pthon3v  30201  umgr2wlk  30207  rusgrnumwlkg  30238  umgrclwwlkge2  30251  clwwlkvbij  30373  0pthonv  30389  1pthon2v  30413  numclwwlkqhash  30635  chscllem4  31901  adjeq  32196  hmopidmchi  32412  xreceu  33154  tocyccntz  33377  archirngz  33422  archiabllem1b  33425  locfinreflem  34147  measvuni  34521  elmbfmvol2  34574  omsmeas  34630  sibfof  34647  eulerpartlemgvv  34683  ballotlemfc0  34800  ballotlemfcc  34801  rankval4b  35408  iccllysconn  35613  cvmliftphtlem  35680  satfv1  35726  sat1el2xp  35742  opnrebl2  36694  re1ax2lem  36760  re1ax2  36761  regsfromregtco  36911  bj-orim2  37010  bj-peircecurry  37012  lindsdom  38125  poimir  38164  volsupnfl  38176  areacirc  38224  totbndbnd  38300  islsati  39630  hdmap14lem2a  42503  rabdiophlem1  43390  pellexlem5  43422  ttac  43625  aomclem4  43646  hbtlem5  43717  idomodle  43780  idomsubgmo  43782  nnoeomeqom  43901  omabs2  43921  rp-isfinite5  44105  iscard4  44121  mnuunid  44851  vk15.4j  45102  ax6e2nd  45132  trsspwALT2  45392  sspwtrALT  45395  sstrALT2  45408  permaxrep  45580  dvmptconst  46487  dvmptidg  46489  fperdvper  46491  dvmulcncf  46497  dvdivcncf  46499  fourierdlem20  46699  fouriercn  46804  ndmaovcl  47795  fundcmpsurinjpreimafv  48012  fmtnofac2  48176  prminf2  48195  gpg5nbgrvtx03starlem1  48688  gpg5nbgrvtx03starlem2  48689  gpg5nbgrvtx03starlem3  48690  gpg5nbgrvtx13starlem1  48691  gpg5nbgrvtx13starlem2  48692  gpg5nbgrvtx13starlem3  48693  gpgprismgr4cyclex  48727  gpg5edgnedg  48750  pgrpgt2nabl  48997  line2x  49385  prstchom2ALT  50193  spcdvw  50308  aacllem  50430