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-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  syl3c  63  mpsyl  65  imp  123  2thd  174  jca  304  syl2anc  408  jc  639  jcnd  641  annimdc  921  orandc  923  dn1dc  944  syl2an23an  1277  xordidc  1377  nfimd  1564  exlimd2  1574  elex22  2701  elex2  2702  spcimdv  2770  spcimedv  2772  rspcdva  2794  elabd  2829  spsbcd  2921  opth  4159  euotd  4176  ssorduni  4403  tfisi  4501  omsinds  4535  nnpredcl  4536  sotri2  4936  sotri3  4937  unielrel  5066  funmo  5138  fnfvima  5652  fliftfun  5697  fliftval  5701  riota5f  5754  riotass2  5756  oprssdmm  6069  tfrlem5  6211  tfrlemibxssdm  6224  tfrlemibfn  6225  tfrlemiex  6228  tfr1onlemsucfn  6237  tfr1onlemsucaccv  6238  tfr1onlembxssdm  6240  tfr1onlembfn  6241  tfr1onlemex  6244  tfr1onlemres  6246  tfrcllemsucfn  6250  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllembfn  6254  tfrcllemex  6257  tfrcllemres  6259  tfrcl  6261  rdgisucinc  6282  frecabex  6295  frecabcl  6296  nntr2  6399  ertr  6444  qliftlem  6507  th3q  6534  resixp  6627  f1dom2g  6650  dom3d  6668  en1  6693  xpdom3m  6728  xpf1o  6738  phplem4dom  6756  phpm  6759  phpelm  6760  findcard  6782  finexdc  6796  fiintim  6817  fisseneq  6820  ssfirab  6822  f1dmvrnfibi  6832  iunfidisj  6834  fidcenumlemrk  6842  suplub2ti  6888  supelti  6889  ordiso2  6920  caseinl  6976  caseinr  6977  djudom  6978  difinfsn  6985  difinfinf  6986  ctm  6994  enumct  7000  ismkvnex  7029  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  acfun  7063  recexnq  7198  ltbtwnnqq  7223  addnnnq0  7257  mulnnnq0  7258  prarloclemn  7307  prarloc  7311  distrlem1prl  7390  distrlem1pru  7391  distrlem4prl  7392  distrlem4pru  7393  ltexprlemrl  7418  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  addsrpr  7553  mulsrpr  7554  map2psrprg  7613  axpre-suploclemres  7709  lemul12a  8620  lemulge11  8624  sup3exmid  8715  nngt0  8745  nn0ge0  9002  nn0ge2m1nn  9037  zletric  9098  zlelttric  9099  nn0n0n1ge2b  9130  nn0ind-raph  9168  supinfneg  9390  infsupneg  9391  rpge0  9454  fz0fzelfz0  9904  fz0fzdiffz0  9907  ige2m2fzo  9975  elfzodifsumelfzo  9978  elfzom1elp1fzo  9979  exfzdc  10017  qletric  10021  qlelttric  10022  rebtwn2zlemshrink  10031  frecuzrdgtcl  10185  frecuzrdg0  10186  frecuzrdgfunlem  10192  frecuzrdg0t  10195  frecuzrdgsuctlem  10196  frecfzennn  10199  seq3f1olemstep  10274  expcl2lemap  10305  leexp1a  10348  expnbnd  10415  faclbnd  10487  faclbnd6  10490  facavg  10492  fihasheqf1oi  10534  fihashf1rn  10535  fihashss  10562  seq3coll  10585  resqrexlemdecn  10784  qabsor  10847  cau3lem  10886  xrmaxiflemab  11016  xrmaxadd  11030  climcn2  11078  sumeq2  11128  sumrbdclem  11146  summodclem3  11149  summodclem2a  11150  zsumdc  11153  fsumgcl  11155  fsum3  11156  isumss  11160  fsumadd  11175  fsum2dlemstep  11203  fisum0diag2  11216  fsummulc2  11217  modfsummodlemstep  11226  fsumabs  11234  fsumrelem  11240  fsumiun  11246  isumshft  11259  mertenslem2  11305  prodeq2  11326  prodrbdclem  11340  prodmodclem3  11344  prodmodclem2a  11345  sin02gt0  11470  efieq1re  11478  dvdsleabs2  11544  4dvdseven  11614  gcdmndc  11637  zsupcllemstep  11638  infssuzex  11642  gcdsupex  11646  gcdsupcl  11647  gcdeq0  11665  gcdaddm  11672  rppwr  11716  algfx  11733  eucalgcvga  11739  lcmmndc  11743  lcmval  11744  lcmcllem  11748  lcmledvds  11751  lcmeq0  11752  qredeq  11777  isprm3  11799  rpexp  11831  sqpweven  11853  2sqpwodd  11854  phicl2  11890  phibnd  11893  phiprmpw  11898  ennnfonelemk  11913  ennnfonelemhom  11928  ennnfonelemrnh  11929  ennnfonelemf1  11931  ctinf  11943  ctiunctlemudc  11950  ctiunctlemf  11951  strslfvd  12000  strslfv2d  12001  strslssd  12005  eltg3  12226  iuncld  12284  cnss2  12396  txcnp  12440  uptx  12443  xblm  12586  metss  12663  fsumcncntop  12725  rescncf  12737  dedekindeulemlu  12768  suplociccex  12772  dedekindicclemlu  12777  dedekindicc  12780  ivthdec  12791  limccnp2lem  12814  dvaddxx  12836  dvmulxx  12837  dvrecap  12846  sumdc2  13006  pwle2  13193  subctctexmid  13196  nninfalllemn  13202  nninfsellemeq  13210  exmidsbthrlem  13217