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 ⊢ (𝜓 → 𝜃)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  spimew  2004  snssg  4747  relcnvtrgOLD  6268  relresfldOLD  6278  onfr  6401  foimacnv  6839  fvi  6958  isoini2  7344  ovidig  7559  f1oexbi  7929  frxp  8128  smores2  8347  tfrlem5  8372  en2sn  9052  en2prd  9058  mapdom1  9144  frfi  9259  fodomfi  9286  ixpfi2  9321  hartogs  9520  wemapsolem  9526  card2on  9530  unwdomg  9560  ttrclss  9703  r1pwss  9770  tz9.12lem3  9775  uniwf  9805  rankval3b  9812  djuun  9935  tskwe  9959  carddomi2  9979  cardsdomelir  9982  infxpenlem  10020  inffien  10070  alephord  10082  alephdom  10088  iunfictbso  10121  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  10575  konigthlem  10581  alephadd  10590  alephexp1  10592  alephreg  10595  pwcfsdom  10596  fpwwe2lem12  10655  gchaleph  10684  gchaleph2  10685  winainflem  10706  inttsk  10787  inar1  10788  inatsk  10791  grudomon  10830  nqerid  10946  nqpr  11027  zmin  12997  uzrdgsuci  14028  isfinite4  14430  pfxccatin12lem3  14805  limsupval2  15571  sumz  15812  fsumsers  15818  isumclim  15847  ntrivcvgfvn0  15992  ntrivcvgtail  15993  zprodn0  16032  iprodclim  16091  alzdvds  16416  bitsfzolem  16530  phicl2  16865  phibnd  16868  pclem  16936  strle1  17256  fnpr2ob  17650  psss  18674  symg2bas  19526  dprdss  20164  irinitoringc  21698  lindsdom  22069  2ndcdisj  23688  dis2ndc  23692  hausmapdom  23732  ptcnplem  23853  fbun  24072  metrest  24756  opnreen  25064  ivthle  25690  ivthle2  25691  ovolfiniun  25735  volfiniun  25781  uniiccdif  25812  uniioovol  25813  uniioombllem4  25820  dyadmbl  25834  vitali  25847  mbflimsup  25900  cpnres  26171  dvcj  26184  dvef  26214  dvne0  26245  lhop2  26249  itgparts  26281  itgsubstlem  26282  ply1divex  26369  fta1blem  26403  dgrlem  26462  pige3ALT  26765  xrlimcnp  27213  ftalem3  27319  lgsdchr  27599  2lgslem1  27638  addsqn2reu  27685  2sqreultblem  27692  2sqreunnltblem  27695  dchrvmasumlem2  27742  pntlem3  27853  mulsproplem13  28401  mulsproplem14  28402  tgisline  28982  axcontlem2  29430  upgrex  29557  umgrnloop2  29611  usgriedgleord  29696  uspgredgleord  29700  nbedgusgr  29840  nb3grprlem2  29849  rusgrnumwrdl2  30054  wlkp1lem2  30140  wwlksnexthasheq  30379  wlksnwwlknvbij  30384  2pthon3v  30419  umgr2wlk  30425  rusgrnumwlkg  30456  umgrclwwlkge2  30469  clwwlkvbij  30591  0pthonv  30607  1pthon2v  30641  numclwwlkqhash  30863  chscllem4  32129  adjeq  32424  hmopidmchi  32640  xreceu  33375  tocyccntz  33592  archirngz  33637  archiabllem1b  33640  locfinreflem  34358  measvuni  34733  elmbfmvol2  34786  omsmeas  34842  sibfof  34859  eulerpartlemgvv  34895  ballotlemfc0  35012  ballotlemfcc  35013  rankval4b  35615  iccllysconn  35837  cvmliftphtlem  35904  satfv1  35950  sat1el2xp  35966  opnrebl2  36948  re1ax2lem  37014  re1ax2  37015  regsfromregtco  37165  bj-orim2  37264  bj-peircecurry  37266  poimir  38410  volsupnfl  38422  areacirc  38470  totbndbnd  38547  islsati  39875  hdmap14lem2a  42748  rabdiophlem1  43650  pellexlem5  43682  ttac  43885  aomclem4  43906  hbtlem5  43977  idomodle  44040  idomsubgmo  44042  nnoeomeqom  44161  omabs2  44181  rp-isfinite5  44365  iscard4  44381  mnuunid  45109  vk15.4j  45359  ax6e2nd  45389  trsspwALT2  45649  sspwtrALT  45652  sstrALT2  45665  permaxrep  45837  dvmptconst  46751  dvmptidg  46753  fperdvper  46755  dvmulcncf  46761  dvdivcncf  46763  fourierdlem20  46963  fouriercn  47068  ndmaovcl  48099  fundcmpsurinjpreimafv  48316  fmtnofac2  48480  prminf2  48499  gpg5nbgrvtx03starlem1  48992  gpg5nbgrvtx03starlem2  48993  gpg5nbgrvtx03starlem3  48994  gpg5nbgrvtx13starlem1  48995  gpg5nbgrvtx13starlem2  48996  gpg5nbgrvtx13starlem3  48997  gpgprismgr4cyclex  49031  gpg5edgnedg  49054  pgrpgt2nabl  49304  line2x  49692  prstchom2ALT  50498  spcdvw  50613  aacllem  50780