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:  spimew  1973  snssg  4727  relcnvtrg  6231  relresfld  6240  onfr  6362  foimacnv  6797  fvi  6916  isoini2  7294  ovidig  7509  f1oexbi  7879  frxp  8076  smores2  8294  tfrlem5  8319  en2sn  8988  en2prd  8994  mapdom1  9080  frfi  9195  fodomfi  9222  fodomfiOLD  9240  ixpfi2  9260  hartogs  9459  wemapsolem  9465  card2on  9469  unwdomg  9499  ttrclss  9641  r1pwss  9708  tz9.12lem3  9713  uniwf  9743  rankval3b  9750  djuun  9850  tskwe  9874  carddomi2  9894  cardsdomelir  9897  infxpenlem  9935  inffien  9985  alephord  9997  alephdom  10003  iunfictbso  10036  dfac8  10058  dfacacn  10064  dfac13  10065  dfac12lem2  10067  infmap2  10139  ackbij1b  10160  ackbij2  10164  fictb  10166  cfslb  10188  fin67  10317  fin1a2lem10  10331  fin1a2lem11  10332  dcomex  10369  ttukeylem1  10431  ttukeylem7  10437  ondomon  10485  konigthlem  10491  alephadd  10500  alephexp1  10502  alephreg  10505  pwcfsdom  10506  fpwwe2lem12  10565  gchaleph  10594  gchaleph2  10595  winainflem  10616  inttsk  10697  inar1  10698  inatsk  10701  grudomon  10740  nqerid  10856  nqpr  10937  zmin  12894  uzrdgsuci  13922  isfinite4  14324  pfxccatin12lem3  14694  limsupval2  15442  sumz  15684  fsumsers  15690  isumclim  15719  ntrivcvgfvn0  15864  ntrivcvgtail  15865  zprodn0  15904  iprodclim  15963  alzdvds  16289  bitsfzolem  16403  phicl2  16738  phibnd  16741  pclem  16809  strle1  17128  fnpr2ob  17522  psss  18546  symg2bas  19368  dprdss  20006  irinitoringc  21459  2ndcdisj  23421  dis2ndc  23425  hausmapdom  23465  ptcnplem  23586  fbun  23805  metrest  24489  opnreen  24797  ivthle  25423  ivthle2  25424  ovolfiniun  25468  volfiniun  25514  uniiccdif  25545  uniioovol  25546  uniioombllem4  25553  dyadmbl  25567  vitali  25580  mbflimsup  25633  cpnres  25904  dvcj  25917  dvef  25947  dvne0  25978  lhop2  25982  itgparts  26014  itgsubstlem  26015  ply1divex  26102  fta1blem  26136  dgrlem  26194  pige3ALT  26484  xrlimcnp  26932  ftalem3  27038  lgsdchr  27318  2lgslem1  27357  addsqn2reu  27404  2sqreultblem  27411  2sqreunnltblem  27414  dchrvmasumlem2  27461  pntlem3  27572  mulsproplem13  28120  mulsproplem14  28121  tgisline  28695  axcontlem2  29034  upgrex  29161  umgrnloop2  29215  usgriedgleord  29297  uspgredgleord  29301  nbedgusgr  29441  nb3grprlem2  29450  rusgrnumwrdl2  29655  wlkp1lem2  29741  wwlksnexthasheq  29971  wlksnwwlknvbij  29976  2pthon3v  30011  umgr2wlk  30017  rusgrnumwlkg  30048  umgrclwwlkge2  30061  clwwlkvbij  30183  0pthonv  30199  1pthon2v  30223  numclwwlkqhash  30445  chscllem4  31711  adjeq  32006  hmopidmchi  32222  xreceu  32981  tocyccntz  33205  archirngz  33250  archiabllem1b  33253  locfinreflem  33984  measvuni  34358  elmbfmvol2  34411  omsmeas  34467  sibfof  34484  eulerpartlemgvv  34520  ballotlemfc0  34637  ballotlemfcc  34638  rankval4b  35243  iccllysconn  35432  cvmliftphtlem  35499  satfv1  35545  sat1el2xp  35561  opnrebl2  36503  re1ax2lem  36569  re1ax2  36570  regsfromregtco  36720  bj-orim2  36820  bj-peircecurry  36822  lindsdom  37935  poimir  37974  volsupnfl  37986  areacirc  38034  totbndbnd  38110  islsati  39440  hdmap14lem2a  42313  rabdiophlem1  43229  pellexlem5  43261  ttac  43464  aomclem4  43485  hbtlem5  43556  idomodle  43619  idomsubgmo  43621  nnoeomeqom  43740  omabs2  43760  rp-isfinite5  43944  iscard4  43960  mnuunid  44704  vk15.4j  44955  ax6e2nd  44985  trsspwALT2  45245  sspwtrALT  45248  sstrALT2  45261  permaxrep  45433  dvmptconst  46343  dvmptidg  46345  fperdvper  46347  dvmulcncf  46353  dvdivcncf  46355  fourierdlem20  46555  fouriercn  46660  ndmaovcl  47651  fundcmpsurinjpreimafv  47868  fmtnofac2  48032  prminf2  48051  gpg5nbgrvtx03starlem1  48544  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx03starlem3  48546  gpg5nbgrvtx13starlem1  48547  gpg5nbgrvtx13starlem2  48548  gpg5nbgrvtx13starlem3  48549  gpgprismgr4cyclex  48583  gpg5edgnedg  48606  pgrpgt2nabl  48842  line2x  49230  prstchom2ALT  50039  spcdvw  50154  aacllem  50276