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  1707  tbwlem2  1708  re1luk3  1714  merco1lem17  1735  re1tbw1  1747  spimew  1975  snssg  4736  relcnvtrg  6209  relresfld  6219  onfr  6346  foimacnv  6789  fvi  6905  isoini2  7271  ovidig  7482  f1oexbi  7848  frxp  8039  smores2  8260  tfrlem5  8286  en2sn  8911  en2snOLD  8912  en2prd  8918  mapdom1  9012  php2OLD  9093  snnen2oOLD  9097  frfi  9158  fodomfi  9195  ixpfi2  9220  hartogs  9406  wemapsolem  9412  card2on  9416  unwdomg  9446  ttrclss  9582  r1pwss  9646  tz9.12lem3  9651  uniwf  9681  rankval3b  9688  djuun  9788  tskwe  9812  carddomi2  9832  cardsdomelir  9835  infxpenlem  9875  inffien  9925  alephord  9937  alephdom  9943  iunfictbso  9976  dfac8  9997  dfacacn  10003  dfac13  10004  dfac12lem2  10006  infmap2  10080  ackbij1b  10101  ackbij2  10105  fictb  10107  cfslb  10128  fin67  10257  fin1a2lem10  10271  fin1a2lem11  10272  dcomex  10309  ttukeylem1  10371  ttukeylem7  10377  ondomon  10425  konigthlem  10430  alephadd  10439  alephexp1  10441  alephreg  10444  pwcfsdom  10445  fpwwe2lem12  10504  gchaleph  10533  gchaleph2  10534  winainflem  10555  inttsk  10636  inar1  10637  inatsk  10640  grudomon  10679  nqerid  10795  nqpr  10876  zmin  12790  uzrdgsuci  13786  isfinite4  14182  pfxccatin12lem3  14544  limsupval2  15289  sumz  15534  fsumsers  15540  isumclim  15569  ntrivcvgfvn0  15711  ntrivcvgtail  15712  zprodn0  15749  iprodclim  15808  alzdvds  16129  bitsfzolem  16241  phicl2  16567  phibnd  16570  pclem  16637  strle1  16957  fnpr2ob  17367  psss  18396  symg2bas  19097  dprdss  19727  2ndcdisj  22713  dis2ndc  22717  hausmapdom  22757  ptcnplem  22878  fbun  23097  metrest  23786  opnreen  24100  ivthle  24726  ivthle2  24727  ovolfiniun  24771  volfiniun  24817  uniiccdif  24848  uniioovol  24849  uniioombllem4  24856  dyadmbl  24870  vitali  24883  mbflimsup  24936  cpnres  25207  dvcj  25220  dvef  25250  dvne0  25281  lhop2  25285  itgparts  25317  itgsubstlem  25318  ply1divex  25407  fta1blem  25439  dgrlem  25496  pige3ALT  25782  xrlimcnp  26224  ftalem3  26330  lgsdchr  26609  2lgslem1  26648  addsqn2reu  26695  2sqreultblem  26702  2sqreunnltblem  26705  dchrvmasumlem2  26752  pntlem3  26863  tgisline  27277  axcontlem2  27622  upgrex  27751  umgrnloop2  27805  usgriedgleord  27884  uspgredgleord  27888  nbedgusgr  28028  nb3grprlem2  28037  rusgrnumwrdl2  28242  wlkp1lem2  28330  wwlksnexthasheq  28556  wlksnwwlknvbij  28561  2pthon3v  28596  umgr2wlk  28602  rusgrnumwlkg  28630  umgrclwwlkge2  28643  clwwlkvbij  28765  0pthonv  28781  1pthon2v  28805  numclwwlkqhash  29027  chscllem4  30290  adjeq  30585  hmopidmchi  30801  xreceu  31481  tocyccntz  31696  archirngz  31728  archiabllem1b  31731  locfinreflem  32086  measvuni  32478  elmbfmvol2  32532  omsmeas  32588  sibfof  32605  eulerpartlemgvv  32641  ballotlemfc0  32757  ballotlemfcc  32758  iccllysconn  33509  cvmliftphtlem  33576  satfv1  33622  sat1el2xp  33638  opnrebl2  34647  re1ax2lem  34713  re1ax2  34714  bj-orim2  34873  bj-peircecurry  34875  lindsdom  35925  poimir  35964  volsupnfl  35976  areacirc  36024  totbndbnd  36101  islsati  37310  hdmap14lem2a  40184  rabdiophlem1  40934  pellexlem5  40966  ttac  41170  aomclem4  41194  hbtlem5  41265  idomodle  41333  idomsubgmo  41335  omabs2  41367  rp-isfinite5  41496  iscard4  41512  mnuunid  42266  vk15.4j  42519  ax6e2nd  42549  trsspwALT2  42810  sspwtrALT  42813  sstrALT2  42826  dvmptconst  43842  dvmptidg  43844  fperdvper  43846  dvmulcncf  43852  dvdivcncf  43854  fourierdlem20  44054  fouriercn  44159  ndmaovcl  45111  fundcmpsurinjpreimafv  45276  fmtnofac2  45437  prminf2  45456  isomuspgrlem2  45701  irinitoringc  46043  pgrpgt2nabl  46118  line2x  46516  prstchom2ALT  46776  spcdvw  46801  aacllem  46921