Theorem sylc 62

Description: A syllogism inference combined with contraction. (Contributed by NM, 4-May-1994.) (Revised by NM, 13-Jul-2013.)

Hypotheses

Ref	Expression
sylc.1	⊢ (𝜑 → 𝜓)
sylc.2	⊢ (𝜑 → 𝜒)
sylc.3	⊢ (𝜓 → (𝜒 → 𝜃))

Assertion

Ref	Expression
sylc	⊢ (𝜑 → 𝜃)

Proof of Theorem sylc

Step	Hyp	Ref	Expression
1		sylc.1	. . 3 ⊢ (𝜑 → 𝜓)
2		sylc.2	. . 3 ⊢ (𝜑 → 𝜒)
3		sylc.3	. . 3 ⊢ (𝜓 → (𝜒 → 𝜃))
4	1, 2, 3	syl2im 38	. 2 ⊢ (𝜑 → (𝜑 → 𝜃))
5	4	pm2.43i 49	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  syl3c  63  mpsyl  65  imp  123  2thd  174  jca  302  syl2anc  406  jc  623  annimdc  902  orandc  904  dn1dc  925  syl2an23an  1258  xordidc  1358  nfimd  1545  exlimd2  1555  elex22  2670  elex2  2671  spcimdv  2739  spcimedv  2741  rspcdva  2763  spsbcd  2888  opth  4117  euotd  4134  ssorduni  4361  tfisi  4459  omsinds  4493  nnpredcl  4494  sotri2  4892  sotri3  4893  unielrel  5022  funmo  5094  fnfvima  5604  fliftfun  5649  fliftval  5653  riota5f  5706  riotass2  5708  oprssdmm  6020  tfrlem5  6162  tfrlemibxssdm  6175  tfrlemibfn  6176  tfrlemiex  6179  tfr1onlemsucfn  6188  tfr1onlemsucaccv  6189  tfr1onlembxssdm  6191  tfr1onlembfn  6192  tfr1onlemex  6195  tfr1onlemres  6197  tfrcllemsucfn  6201  tfrcllemsucaccv  6202  tfrcllembxssdm  6204  tfrcllembfn  6205  tfrcllemex  6208  tfrcllemres  6210  tfrcl  6212  rdgisucinc  6233  frecabex  6246  frecabcl  6247  nntr2  6350  ertr  6395  qliftlem  6458  th3q  6485  resixp  6578  f1dom2g  6601  dom3d  6619  en1  6644  xpdom3m  6678  xpf1o  6688  phplem4dom  6706  phpm  6709  phpelm  6710  findcard  6732  finexdc  6746  fiintim  6767  fisseneq  6770  ssfirab  6771  f1dmvrnfibi  6781  iunfidisj  6783  fidcenumlemrk  6791  suplub2ti  6837  supelti  6838  ordiso2  6869  caseinl  6925  caseinr  6926  djudom  6927  difinfsn  6934  difinfinf  6935  ctm  6943  enumct  6949  exmidfodomrlemr  7002  exmidfodomrlemrALT  7003  acfun  7007  recexnq  7139  ltbtwnnqq  7164  addnnnq0  7198  mulnnnq0  7199  prarloclemn  7248  prarloc  7252  distrlem1prl  7331  distrlem1pru  7332  distrlem4prl  7333  distrlem4pru  7334  ltexprlemrl  7359  cauappcvgprlemladdru  7405  cauappcvgprlemladdrl  7406  addsrpr  7481  mulsrpr  7482  lemul12a  8523  lemulge11  8527  sup3exmid  8618  nngt0  8648  nn0ge0  8899  nn0ge2m1nn  8934  zletric  8995  zlelttric  8996  nn0n0n1ge2b  9027  nn0ind-raph  9065  supinfneg  9285  infsupneg  9286  rpge0  9348  fz0fzelfz0  9790  fz0fzdiffz0  9793  ige2m2fzo  9861  elfzodifsumelfzo  9864  elfzom1elp1fzo  9865  exfzdc  9903  qletric  9907  qlelttric  9908  rebtwn2zlemshrink  9917  frecuzrdgtcl  10071  frecuzrdg0  10072  frecuzrdgfunlem  10078  frecuzrdg0t  10081  frecuzrdgsuctlem  10082  frecfzennn  10085  seq3f1olemstep  10160  expcl2lemap  10191  leexp1a  10234  expnbnd  10301  faclbnd  10373  faclbnd6  10376  facavg  10378  fihasheqf1oi  10420  fihashf1rn  10421  fihashss  10448  seq3coll  10471  resqrexlemdecn  10669  qabsor  10732  cau3lem  10771  xrmaxiflemab  10901  xrmaxadd  10915  climcn2  10963  sumeq2  11013  sumrbdclem  11030  summodclem3  11034  summodclem2a  11035  zsumdc  11038  fsumgcl  11040  fsum3  11041  isumss  11045  fsumadd  11060  fsum2dlemstep  11088  fisum0diag2  11101  fsummulc2  11102  modfsummodlemstep  11111  fsumabs  11119  fsumrelem  11125  fsumiun  11131  isumshft  11144  mertenslem2  11190  sin02gt0  11314  efieq1re  11321  dvdsleabs2  11385  4dvdseven  11455  gcdmndc  11478  zsupcllemstep  11479  infssuzex  11483  gcdsupex  11487  gcdsupcl  11488  gcdeq0  11506  gcdaddm  11513  rppwr  11555  algfx  11572  eucalgcvga  11578  lcmmndc  11582  lcmval  11583  lcmcllem  11587  lcmledvds  11590  lcmeq0  11591  qredeq  11616  isprm3  11638  rpexp  11670  sqpweven  11691  2sqpwodd  11692  phicl2  11728  phibnd  11731  phiprmpw  11736  ennnfonelemk  11751  ennnfonelemhom  11766  ennnfonelemrnh  11767  ennnfonelemf1  11769  ctinf  11781  ctiunctlemudc  11786  ctiunctlemf  11787  strslfvd  11836  strslfv2d  11837  strslssd  11841  eltg3  12062  iuncld  12120  cnss2  12231  txcnp  12275  uptx  12278  xblm  12399  metss  12476  fsumcncntop  12535  rescncf  12547  limccnp2lem  12594  sumdc2  12685  pwle2  12872  nninfalllemn  12879  nninfsellemeq  12887  exmidsbthrlem  12894