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:  tbwlem1  1700  tbwlem2  1701  re1luk3  1707  merco1lem17  1728  re1tbw1  1740  spimew  1968  snssg  4792  relcnvtrg  6277  relresfld  6287  onfr  6415  foimacnv  6860  fvi  6978  isoini2  7351  ovidig  7568  f1oexbi  7941  frxp  8140  smores2  8384  tfrlem5  8410  en2sn  9077  en2snOLD  9078  en2prd  9086  mapdom1  9180  php2OLD  9257  snnen2oOLD  9261  frfi  9322  fodomfi  9352  fodomfiOLD  9372  ixpfi2  9394  hartogs  9587  wemapsolem  9593  card2on  9597  unwdomg  9627  ttrclss  9763  r1pwss  9827  tz9.12lem3  9832  uniwf  9862  rankval3b  9869  djuun  9969  tskwe  9993  carddomi2  10013  cardsdomelir  10016  infxpenlem  10056  inffien  10106  alephord  10118  alephdom  10124  iunfictbso  10157  dfac8  10178  dfacacn  10184  dfac13  10185  dfac12lem2  10187  infmap2  10261  ackbij1b  10282  ackbij2  10286  fictb  10288  cfslb  10309  fin67  10438  fin1a2lem10  10452  fin1a2lem11  10453  dcomex  10490  ttukeylem1  10552  ttukeylem7  10558  ondomon  10606  konigthlem  10611  alephadd  10620  alephexp1  10622  alephreg  10625  pwcfsdom  10626  fpwwe2lem12  10685  gchaleph  10714  gchaleph2  10715  winainflem  10736  inttsk  10817  inar1  10818  inatsk  10821  grudomon  10860  nqerid  10976  nqpr  11057  zmin  12980  uzrdgsuci  13980  isfinite4  14379  pfxccatin12lem3  14740  limsupval2  15482  sumz  15726  fsumsers  15732  isumclim  15761  ntrivcvgfvn0  15903  ntrivcvgtail  15904  zprodn0  15941  iprodclim  16000  alzdvds  16322  bitsfzolem  16434  phicl2  16770  phibnd  16773  pclem  16840  strle1  17160  fnpr2ob  17573  psss  18605  symg2bas  19390  dprdss  20029  irinitoringc  21469  2ndcdisj  23451  dis2ndc  23455  hausmapdom  23495  ptcnplem  23616  fbun  23835  metrest  24524  opnreen  24838  ivthle  25476  ivthle2  25477  ovolfiniun  25521  volfiniun  25567  uniiccdif  25598  uniioovol  25599  uniioombllem4  25606  dyadmbl  25620  vitali  25633  mbflimsup  25686  cpnres  25958  dvcj  25973  dvef  26003  dvne0  26035  lhop2  26039  itgparts  26073  itgsubstlem  26074  ply1divex  26164  fta1blem  26198  dgrlem  26256  pige3ALT  26547  xrlimcnp  26996  ftalem3  27103  lgsdchr  27384  2lgslem1  27423  addsqn2reu  27470  2sqreultblem  27477  2sqreunnltblem  27480  dchrvmasumlem2  27527  pntlem3  27638  mulsproplem13  28129  mulsproplem14  28130  tgisline  28554  axcontlem2  28899  upgrex  29028  umgrnloop2  29082  usgriedgleord  29164  uspgredgleord  29168  nbedgusgr  29308  nb3grprlem2  29317  rusgrnumwrdl2  29523  wlkp1lem2  29611  wwlksnexthasheq  29837  wlksnwwlknvbij  29842  2pthon3v  29877  umgr2wlk  29883  rusgrnumwlkg  29911  umgrclwwlkge2  29924  clwwlkvbij  30046  0pthonv  30062  1pthon2v  30086  numclwwlkqhash  30308  chscllem4  31573  adjeq  31868  hmopidmchi  32084  xreceu  32783  tocyccntz  33022  archirngz  33054  archiabllem1b  33057  locfinreflem  33655  measvuni  34047  elmbfmvol2  34101  omsmeas  34157  sibfof  34174  eulerpartlemgvv  34210  ballotlemfc0  34326  ballotlemfcc  34327  iccllysconn  35078  cvmliftphtlem  35145  satfv1  35191  sat1el2xp  35207  opnrebl2  36033  re1ax2lem  36099  re1ax2  36100  bj-orim2  36259  bj-peircecurry  36261  lindsdom  37315  poimir  37354  volsupnfl  37366  areacirc  37414  totbndbnd  37490  islsati  38692  hdmap14lem2a  41566  rabdiophlem1  42458  pellexlem5  42490  ttac  42694  aomclem4  42718  hbtlem5  42789  idomodle  42856  idomsubgmo  42858  nnoeomeqom  42978  omabs2  42998  rp-isfinite5  43184  iscard4  43200  mnuunid  43951  vk15.4j  44204  ax6e2nd  44234  trsspwALT2  44495  sspwtrALT  44498  sstrALT2  44511  dvmptconst  45536  dvmptidg  45538  fperdvper  45540  dvmulcncf  45546  dvdivcncf  45548  fourierdlem20  45748  fouriercn  45853  ndmaovcl  46816  fundcmpsurinjpreimafv  46980  fmtnofac2  47141  prminf2  47160  pgrpgt2nabl  47745  line2x  48142  prstchom2ALT  48400  spcdvw  48425  aacllem  48549