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  1971  snssg  4750  relcnvtrg  6242  relresfld  6252  onfr  6374  foimacnv  6820  fvi  6940  isoini2  7317  ovidig  7534  f1oexbi  7907  frxp  8108  smores2  8326  tfrlem5  8351  en2sn  9015  en2prd  9022  mapdom1  9112  frfi  9239  fodomfi  9268  fodomfiOLD  9288  ixpfi2  9308  hartogs  9504  wemapsolem  9510  card2on  9514  unwdomg  9544  ttrclss  9680  r1pwss  9744  tz9.12lem3  9749  uniwf  9779  rankval3b  9786  djuun  9886  tskwe  9910  carddomi2  9930  cardsdomelir  9933  infxpenlem  9973  inffien  10023  alephord  10035  alephdom  10041  iunfictbso  10074  dfac8  10096  dfacacn  10102  dfac13  10103  dfac12lem2  10105  infmap2  10177  ackbij1b  10198  ackbij2  10202  fictb  10204  cfslb  10226  fin67  10355  fin1a2lem10  10369  fin1a2lem11  10370  dcomex  10407  ttukeylem1  10469  ttukeylem7  10475  ondomon  10523  konigthlem  10528  alephadd  10537  alephexp1  10539  alephreg  10542  pwcfsdom  10543  fpwwe2lem12  10602  gchaleph  10631  gchaleph2  10632  winainflem  10653  inttsk  10734  inar1  10735  inatsk  10738  grudomon  10777  nqerid  10893  nqpr  10974  zmin  12910  uzrdgsuci  13932  isfinite4  14334  pfxccatin12lem3  14704  limsupval2  15453  sumz  15695  fsumsers  15701  isumclim  15730  ntrivcvgfvn0  15872  ntrivcvgtail  15873  zprodn0  15912  iprodclim  15971  alzdvds  16297  bitsfzolem  16411  phicl2  16745  phibnd  16748  pclem  16816  strle1  17135  fnpr2ob  17528  psss  18546  symg2bas  19330  dprdss  19968  irinitoringc  21396  2ndcdisj  23350  dis2ndc  23354  hausmapdom  23394  ptcnplem  23515  fbun  23734  metrest  24419  opnreen  24727  ivthle  25364  ivthle2  25365  ovolfiniun  25409  volfiniun  25455  uniiccdif  25486  uniioovol  25487  uniioombllem4  25494  dyadmbl  25508  vitali  25521  mbflimsup  25574  cpnres  25846  dvcj  25861  dvef  25891  dvne0  25923  lhop2  25927  itgparts  25961  itgsubstlem  25962  ply1divex  26049  fta1blem  26083  dgrlem  26141  pige3ALT  26436  xrlimcnp  26885  ftalem3  26992  lgsdchr  27273  2lgslem1  27312  addsqn2reu  27359  2sqreultblem  27366  2sqreunnltblem  27369  dchrvmasumlem2  27416  pntlem3  27527  mulsproplem13  28038  mulsproplem14  28039  tgisline  28561  axcontlem2  28899  upgrex  29026  umgrnloop2  29080  usgriedgleord  29162  uspgredgleord  29166  nbedgusgr  29306  nb3grprlem2  29315  rusgrnumwrdl2  29521  wlkp1lem2  29609  wwlksnexthasheq  29840  wlksnwwlknvbij  29845  2pthon3v  29880  umgr2wlk  29886  rusgrnumwlkg  29914  umgrclwwlkge2  29927  clwwlkvbij  30049  0pthonv  30065  1pthon2v  30089  numclwwlkqhash  30311  chscllem4  31576  adjeq  31871  hmopidmchi  32087  xreceu  32849  tocyccntz  33108  archirngz  33150  archiabllem1b  33153  locfinreflem  33837  measvuni  34211  elmbfmvol2  34265  omsmeas  34321  sibfof  34338  eulerpartlemgvv  34374  ballotlemfc0  34491  ballotlemfcc  34492  iccllysconn  35244  cvmliftphtlem  35311  satfv1  35357  sat1el2xp  35373  opnrebl2  36316  re1ax2lem  36382  re1ax2  36383  bj-orim2  36551  bj-peircecurry  36553  lindsdom  37615  poimir  37654  volsupnfl  37666  areacirc  37714  totbndbnd  37790  islsati  38994  hdmap14lem2a  41868  rabdiophlem1  42796  pellexlem5  42828  ttac  43032  aomclem4  43053  hbtlem5  43124  idomodle  43187  idomsubgmo  43189  nnoeomeqom  43308  omabs2  43328  rp-isfinite5  43513  iscard4  43529  mnuunid  44273  vk15.4j  44525  ax6e2nd  44555  trsspwALT2  44815  sspwtrALT  44818  sstrALT2  44831  permaxrep  45003  dvmptconst  45920  dvmptidg  45922  fperdvper  45924  dvmulcncf  45930  dvdivcncf  45932  fourierdlem20  46132  fouriercn  46237  ndmaovcl  47208  fundcmpsurinjpreimafv  47413  fmtnofac2  47574  prminf2  47593  gpg5nbgrvtx03starlem1  48063  gpg5nbgrvtx03starlem2  48064  gpg5nbgrvtx03starlem3  48065  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem2  48067  gpg5nbgrvtx13starlem3  48068  gpgprismgr4cyclex  48101  pgrpgt2nabl  48358  line2x  48747  prstchom2ALT  49557  spcdvw  49672  aacllem  49794