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  4754  relcnvtrgOLD  6274  relresfldOLD  6284  onfr  6407  foimacnv  6845  fvi  6964  isoini2  7348  ovidig  7565  f1oexbi  7934  frxp  8131  smores2  8350  tfrlem5  8375  en2sn  9048  en2prd  9054  mapdom1  9140  frfi  9255  fodomfi  9282  ixpfi2  9317  hartogs  9516  wemapsolem  9522  card2on  9526  unwdomg  9556  ttrclss  9699  r1pwss  9766  tz9.12lem3  9771  uniwf  9801  rankval3b  9808  djuun  9931  tskwe  9955  carddomi2  9975  cardsdomelir  9978  infxpenlem  10016  inffien  10066  alephord  10078  alephdom  10084  iunfictbso  10117  dfac8  10138  dfacacn  10144  dfac13  10145  dfac12lem2  10147  infmap2  10219  ackbij1b  10240  ackbij2  10244  fictb  10246  cfslb  10268  fin67  10397  fin1a2lem10  10411  fin1a2lem11  10412  dcomex  10449  ttukeylem1  10511  ttukeylem7  10517  ondomon  10565  konigthlem  10571  alephadd  10580  alephexp1  10582  alephreg  10585  pwcfsdom  10586  fpwwe2lem12  10645  gchaleph  10674  gchaleph2  10675  winainflem  10696  inttsk  10777  inar1  10778  inatsk  10781  grudomon  10820  nqerid  10936  nqpr  11017  zmin  12986  uzrdgsuci  14016  isfinite4  14418  pfxccatin12lem3  14793  limsupval2  15557  sumz  15799  fsumsers  15805  isumclim  15834  ntrivcvgfvn0  15979  ntrivcvgtail  15980  zprodn0  16019  iprodclim  16078  alzdvds  16403  bitsfzolem  16517  phicl2  16852  phibnd  16855  pclem  16923  strle1  17243  fnpr2ob  17637  psss  18661  symg2bas  19494  dprdss  20132  irinitoringc  21666  2ndcdisj  23650  dis2ndc  23654  hausmapdom  23694  ptcnplem  23815  fbun  24034  metrest  24718  opnreen  25026  ivthle  25652  ivthle2  25653  ovolfiniun  25697  volfiniun  25743  uniiccdif  25774  uniioovol  25775  uniioombllem4  25782  dyadmbl  25796  vitali  25809  mbflimsup  25862  cpnres  26133  dvcj  26146  dvef  26176  dvne0  26207  lhop2  26211  itgparts  26243  itgsubstlem  26244  ply1divex  26331  fta1blem  26365  dgrlem  26423  pige3ALT  26722  xrlimcnp  27170  ftalem3  27276  lgsdchr  27556  2lgslem1  27595  addsqn2reu  27642  2sqreultblem  27649  2sqreunnltblem  27652  dchrvmasumlem2  27699  pntlem3  27810  mulsproplem13  28358  mulsproplem14  28359  tgisline  28937  axcontlem2  29352  upgrex  29479  umgrnloop2  29533  usgriedgleord  29615  uspgredgleord  29619  nbedgusgr  29759  nb3grprlem2  29768  rusgrnumwrdl2  29973  wlkp1lem2  30059  wwlksnexthasheq  30289  wlksnwwlknvbij  30294  2pthon3v  30329  umgr2wlk  30335  rusgrnumwlkg  30366  umgrclwwlkge2  30379  clwwlkvbij  30501  0pthonv  30517  1pthon2v  30541  numclwwlkqhash  30763  chscllem4  32029  adjeq  32324  hmopidmchi  32540  xreceu  33278  tocyccntz  33495  archirngz  33540  archiabllem1b  33543  locfinreflem  34261  measvuni  34636  elmbfmvol2  34689  omsmeas  34745  sibfof  34762  eulerpartlemgvv  34798  ballotlemfc0  34915  ballotlemfcc  34916  rankval4b  35518  iccllysconn  35763  cvmliftphtlem  35830  satfv1  35876  sat1el2xp  35892  opnrebl2  36873  re1ax2lem  36939  re1ax2  36940  regsfromregtco  37090  bj-orim2  37189  bj-peircecurry  37191  lindsdom  38306  poimir  38345  volsupnfl  38357  areacirc  38405  totbndbnd  38481  islsati  39809  hdmap14lem2a  42682  rabdiophlem1  43569  pellexlem5  43601  ttac  43804  aomclem4  43825  hbtlem5  43896  idomodle  43959  idomsubgmo  43961  nnoeomeqom  44080  omabs2  44100  rp-isfinite5  44284  iscard4  44300  mnuunid  45028  vk15.4j  45278  ax6e2nd  45308  trsspwALT2  45568  sspwtrALT  45571  sstrALT2  45584  permaxrep  45756  dvmptconst  46670  dvmptidg  46672  fperdvper  46674  dvmulcncf  46680  dvdivcncf  46682  fourierdlem20  46882  fouriercn  46987  ndmaovcl  47981  fundcmpsurinjpreimafv  48198  fmtnofac2  48362  prminf2  48381  gpg5nbgrvtx03starlem1  48874  gpg5nbgrvtx03starlem2  48875  gpg5nbgrvtx03starlem3  48876  gpg5nbgrvtx13starlem1  48877  gpg5nbgrvtx13starlem2  48878  gpg5nbgrvtx13starlem3  48879  gpgprismgr4cyclex  48913  gpg5edgnedg  48936  pgrpgt2nabl  49187  line2x  49575  prstchom2ALT  50383  spcdvw  50498  aacllem  50662