Theorem mpsyl 69

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 66	1 ⊢ (𝜓 → 𝜃)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  spimew  2004  snssg  4744  relcnvtrgOLD  6262  relresfldOLD  6272  onfr  6395  foimacnv  6834  fvi  6953  isoini2  7339  ovidig  7554  f1oexbi  7929  frxp  8127  smores2  8346  tfrlem5  8371  en2sn  9053  en2prd  9059  mapdom1  9145  frfi  9260  fodomfi  9288  ixpfi2  9323  hartogs  9522  wemapsolem  9528  card2on  9532  unwdomg  9562  ttrclss  9705  r1pwss  9774  tz9.12lem3  9779  uniwf  9809  rankval3b  9817  rankval4b  9861  spcdvw  9951  djuun  9988  tskwe  10012  carddomi2  10032  cardsdomelir  10035  infxpenlem  10073  inffien  10123  alephord  10135  alephdom  10141  iunfictbso  10174  dfac8  10195  dfacacn  10201  dfac13  10202  dfac12lem2  10204  infmap2  10276  ackbij1b  10297  ackbij2  10301  fictb  10303  cfslb  10325  fin67  10454  fin1a2lem10  10468  fin1a2lem11  10469  dcomex  10506  ttukeylem1  10568  ttukeylem7  10574  ondomon  10628  konigthlem  10634  alephadd  10643  alephexp1  10645  alephreg  10648  pwcfsdom  10649  fpwwe2lem12  10708  gchaleph  10737  gchaleph2  10738  winainflem  10759  inttsk  10840  inar1  10841  inatsk  10844  grudomon  10883  nqerid  10999  nqpr  11080  zmin  13052  uzrdgsuci  14083  isfinite4  14486  pfxccatin12lem3  14861  limsupval2  15627  sumz  15868  fsumsers  15874  isumclim  15903  ntrivcvgfvn0  16048  ntrivcvgtail  16049  zprodn0  16086  iprodclim  16145  alzdvds  16470  bitsfzolem  16584  phicl2  16925  phibnd  16928  pclem  16996  strle1  17316  fnpr2ob  17710  psss  18734  symg2bas  19587  dprdss  20225  irinitoringc  21765  lindsdom  22136  2ndcdisj  23755  dis2ndc  23759  hausmapdom  23799  ptcnplem  23920  fbun  24139  metrest  24823  opnreen  25131  ivthle  25757  ivthle2  25758  ovolfiniun  25802  volfiniun  25848  uniiccdif  25879  uniioovol  25880  uniioombllem4  25887  dyadmbl  25901  vitali  25914  mbflimsup  25967  cpnres  26237  dvcj  26250  dvef  26280  dvne0  26311  lhop2  26315  itgparts  26347  itgsubstlem  26348  ply1divex  26435  fta1blem  26469  dgrlem  26528  pige3ALT  26830  xrlimcnp  27278  ftalem3  27384  lgsdchr  27664  2lgslem1  27703  addsqn2reu  27750  2sqreultblem  27757  2sqreunnltblem  27760  dchrvmasumlem2  27807  pntlem3  27918  mulsproplem13  28496  mulsproplem14  28497  tgisline  29077  axcontlem2  29525  upgrex  29652  umgrnloop2  29706  usgriedgleord  29791  uspgredgleord  29795  nbedgusgr  29935  nb3grprlem2  29944  rusgrnumwrdl2  30149  wlkp1lem2  30235  wwlksnexthasheq  30474  wlksnwwlknvbij  30479  2pthon3v  30514  umgr2wlk  30520  rusgrnumwlkg  30551  umgrclwwlkge2  30564  clwwlkvbij  30686  0pthonv  30702  1pthon2v  30736  numclwwlkqhash  30958  chscllem4  32224  adjeq  32519  hmopidmchi  32735  xreceu  33470  tocyccntz  33687  archirngz  33732  archiabllem1b  33735  locfinreflem  34454  measvuni  34829  elmbfmvol2  34882  omsmeas  34938  sibfof  34955  eulerpartlemgvv  34991  ballotlemfc0  35108  ballotlemfcc  35109  iccllysconn  35984  cvmliftphtlem  36051  satfv1  36097  sat1el2xp  36113  opnrebl2  37079  re1ax2lem  37145  re1ax2  37146  regsfromregtco  37296  bj-orim2  37395  bj-peircecurry  37397  poimir  38539  volsupnfl  38551  areacirc  38599  totbndbnd  38691  islsati  40019  hdmap14lem2a  42892  rabdiophlem1  43761  pellexlem5  43793  ttac  43996  aomclem4  44017  hbtlem5  44088  idomodle  44151  idomsubgmo  44153  nnoeomeqom  44272  omabs2  44292  rp-isfinite5  44476  iscard4  44492  mnuunid  45220  vk15.4j  45470  ax6e2nd  45500  trsspwALT2  45760  sspwtrALT  45763  sstrALT2  45776  permaxrep  45948  dvmptconst  46869  dvmptidg  46871  fperdvper  46873  dvmulcncf  46879  dvdivcncf  46881  fourierdlem20  47081  fouriercn  47186  ndmaovcl  48217  fundcmpsurinjpreimafv  48434  fmtnofac2  48598  prminf2  48617  gpg5nbgrvtx03starlem1  49110  gpg5nbgrvtx03starlem2  49111  gpg5nbgrvtx03starlem3  49112  gpg5nbgrvtx13starlem1  49113  gpg5nbgrvtx13starlem2  49114  gpg5nbgrvtx13starlem3  49115  gpgprismgr4cyclex  49149  gpg5edgnedg  49172  pgrpgt2nabl  49422  line2x  49810  prstchom2ALT  50616  aacllem  50883