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  1708  tbwlem2  1709  re1luk3  1715  merco1lem17  1736  re1tbw1  1748  spimew  1976  snssg  4788  relcnvtrg  6266  relresfld  6276  onfr  6404  foimacnv  6851  fvi  6968  isoini2  7336  ovidig  7550  f1oexbi  7919  frxp  8112  smores2  8354  tfrlem5  8380  en2sn  9041  en2snOLD  9042  en2prd  9048  mapdom1  9142  php2OLD  9223  snnen2oOLD  9227  frfi  9288  fodomfi  9325  ixpfi2  9350  hartogs  9539  wemapsolem  9545  card2on  9549  unwdomg  9579  ttrclss  9715  r1pwss  9779  tz9.12lem3  9784  uniwf  9814  rankval3b  9821  djuun  9921  tskwe  9945  carddomi2  9965  cardsdomelir  9968  infxpenlem  10008  inffien  10058  alephord  10070  alephdom  10076  iunfictbso  10109  dfac8  10130  dfacacn  10136  dfac13  10137  dfac12lem2  10139  infmap2  10213  ackbij1b  10234  ackbij2  10238  fictb  10240  cfslb  10261  fin67  10390  fin1a2lem10  10404  fin1a2lem11  10405  dcomex  10442  ttukeylem1  10504  ttukeylem7  10510  ondomon  10558  konigthlem  10563  alephadd  10572  alephexp1  10574  alephreg  10577  pwcfsdom  10578  fpwwe2lem12  10637  gchaleph  10666  gchaleph2  10667  winainflem  10688  inttsk  10769  inar1  10770  inatsk  10773  grudomon  10812  nqerid  10928  nqpr  11009  zmin  12928  uzrdgsuci  13925  isfinite4  14322  pfxccatin12lem3  14682  limsupval2  15424  sumz  15668  fsumsers  15674  isumclim  15703  ntrivcvgfvn0  15845  ntrivcvgtail  15846  zprodn0  15883  iprodclim  15942  alzdvds  16263  bitsfzolem  16375  phicl2  16701  phibnd  16704  pclem  16771  strle1  17091  fnpr2ob  17504  psss  18533  symg2bas  19260  dprdss  19899  2ndcdisj  22960  dis2ndc  22964  hausmapdom  23004  ptcnplem  23125  fbun  23344  metrest  24033  opnreen  24347  ivthle  24973  ivthle2  24974  ovolfiniun  25018  volfiniun  25064  uniiccdif  25095  uniioovol  25096  uniioombllem4  25103  dyadmbl  25117  vitali  25130  mbflimsup  25183  cpnres  25454  dvcj  25467  dvef  25497  dvne0  25528  lhop2  25532  itgparts  25564  itgsubstlem  25565  ply1divex  25654  fta1blem  25686  dgrlem  25743  pige3ALT  26029  xrlimcnp  26473  ftalem3  26579  lgsdchr  26858  2lgslem1  26897  addsqn2reu  26944  2sqreultblem  26951  2sqreunnltblem  26954  dchrvmasumlem2  27001  pntlem3  27112  mulsproplem13  27584  mulsproplem14  27585  tgisline  27878  axcontlem2  28223  upgrex  28352  umgrnloop2  28406  usgriedgleord  28485  uspgredgleord  28489  nbedgusgr  28629  nb3grprlem2  28638  rusgrnumwrdl2  28843  wlkp1lem2  28931  wwlksnexthasheq  29157  wlksnwwlknvbij  29162  2pthon3v  29197  umgr2wlk  29203  rusgrnumwlkg  29231  umgrclwwlkge2  29244  clwwlkvbij  29366  0pthonv  29382  1pthon2v  29406  numclwwlkqhash  29628  chscllem4  30893  adjeq  31188  hmopidmchi  31404  xreceu  32088  tocyccntz  32303  archirngz  32335  archiabllem1b  32338  locfinreflem  32820  measvuni  33212  elmbfmvol2  33266  omsmeas  33322  sibfof  33339  eulerpartlemgvv  33375  ballotlemfc0  33491  ballotlemfcc  33492  iccllysconn  34241  cvmliftphtlem  34308  satfv1  34354  sat1el2xp  34370  opnrebl2  35206  re1ax2lem  35272  re1ax2  35273  bj-orim2  35432  bj-peircecurry  35434  lindsdom  36482  poimir  36521  volsupnfl  36533  areacirc  36581  totbndbnd  36657  islsati  37864  hdmap14lem2a  40738  rabdiophlem1  41539  pellexlem5  41571  ttac  41775  aomclem4  41799  hbtlem5  41870  idomodle  41938  idomsubgmo  41940  nnoeomeqom  42062  omabs2  42082  rp-isfinite5  42268  iscard4  42284  mnuunid  43036  vk15.4j  43289  ax6e2nd  43319  trsspwALT2  43580  sspwtrALT  43583  sstrALT2  43596  dvmptconst  44631  dvmptidg  44633  fperdvper  44635  dvmulcncf  44641  dvdivcncf  44643  fourierdlem20  44843  fouriercn  44948  ndmaovcl  45911  fundcmpsurinjpreimafv  46076  fmtnofac2  46237  prminf2  46256  isomuspgrlem2  46501  irinitoringc  46967  pgrpgt2nabl  47042  line2x  47440  prstchom2ALT  47699  spcdvw  47724  aacllem  47848