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  409  jc  640  jcnd  642  annimdc  927  orandc  929  dn1dc  950  syl2an23an  1289  xordidc  1389  nfimd  1573  exlimd2  1583  elex22  2741  elex2  2742  spcimdv  2810  spcimedv  2812  spcedv  2815  rspcdva  2835  elabd  2871  spsbcd  2963  opth  4215  euotd  4232  ssorduni  4464  tfisi  4564  omsinds  4599  nnpredcl  4600  sotri2  5001  sotri3  5002  unielrel  5131  funmo  5203  fnfvima  5719  fliftfun  5764  fliftval  5768  riota5f  5822  riotass2  5824  oprssdmm  6139  tfrlem5  6282  tfrlemibxssdm  6295  tfrlemibfn  6296  tfrlemiex  6299  tfr1onlemsucfn  6308  tfr1onlemsucaccv  6309  tfr1onlembxssdm  6311  tfr1onlembfn  6312  tfr1onlemex  6315  tfr1onlemres  6317  tfrcllemsucfn  6321  tfrcllemsucaccv  6322  tfrcllembxssdm  6324  tfrcllembfn  6325  tfrcllemex  6328  tfrcllemres  6330  tfrcl  6332  rdgisucinc  6353  frecabex  6366  frecabcl  6367  nntr2  6471  ertr  6516  qliftlem  6579  th3q  6606  resixp  6699  f1dom2g  6722  dom3d  6740  en1  6765  xpdom3m  6800  xpf1o  6810  phplem4dom  6828  phpm  6831  phpelm  6832  findcard  6854  finexdc  6868  fiintim  6894  fisseneq  6897  ssfirab  6899  f1dmvrnfibi  6909  iunfidisj  6911  fidcenumlemrk  6919  dcfi  6946  suplub2ti  6966  supelti  6967  ordiso2  7000  caseinl  7056  caseinr  7057  djudom  7058  difinfsn  7065  difinfinf  7066  ctm  7074  enumct  7080  nnnninfeq  7092  ismkvnex  7119  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  acfun  7163  exmidontriimlem2  7178  exmidontriimlem3  7179  cc2lem  7207  cc3  7209  recexnq  7331  ltbtwnnqq  7356  addnnnq0  7390  mulnnnq0  7391  prarloclemn  7440  prarloc  7444  distrlem1prl  7523  distrlem1pru  7524  distrlem4prl  7525  distrlem4pru  7526  ltexprlemrl  7551  cauappcvgprlemladdru  7597  cauappcvgprlemladdrl  7598  addsrpr  7686  mulsrpr  7687  map2psrprg  7746  axpre-suploclemres  7842  lemul12a  8757  lemulge11  8761  sup3exmid  8852  nngt0  8882  nn0ge0  9139  nn0ge2m1nn  9174  zletric  9235  zlelttric  9236  nn0n0n1ge2b  9270  nn0ind-raph  9308  supinfneg  9533  infsupneg  9534  infregelbex  9536  rpge0  9602  fz0fzelfz0  10062  fz0fzdiffz0  10065  ige2m2fzo  10133  elfzodifsumelfzo  10136  elfzom1elp1fzo  10137  exfzdc  10175  qletric  10179  qlelttric  10180  rebtwn2zlemshrink  10189  frecuzrdgtcl  10347  frecuzrdg0  10348  frecuzrdgfunlem  10354  frecuzrdg0t  10357  frecuzrdgsuctlem  10358  frecfzennn  10361  seq3f1olemstep  10436  expcl2lemap  10467  leexp1a  10510  expnbnd  10578  faclbnd  10654  faclbnd6  10657  facavg  10659  fihasheqf1oi  10701  fihashf1rn  10702  fihashss  10729  fiubm  10741  seq3coll  10755  resqrexlemdecn  10954  qabsor  11017  cau3lem  11056  xrmaxiflemab  11188  xrmaxadd  11202  climcn2  11250  sumeq2  11300  sumrbdclem  11318  summodclem3  11321  summodclem2a  11322  zsumdc  11325  fsumgcl  11327  fsum3  11328  isumss  11332  fsumadd  11347  fsum2dlemstep  11375  fisum0diag2  11388  fsummulc2  11389  modfsummodlemstep  11398  fsumabs  11406  fsumrelem  11412  fsumiun  11418  isumshft  11431  mertenslem2  11477  prodeq2  11498  prodrbdclem  11512  prodmodclem3  11516  prodmodclem2a  11517  zproddc  11520  fprodseq  11524  fprodmul  11532  fprodconst  11561  fprodap0  11562  fprod2dlemstep  11563  fprodrec  11570  fprodsplit1f  11575  fprodap0f  11577  fprodle  11581  sin02gt0  11704  efieq1re  11712  p1modz1  11734  dvdsleabs2  11784  4dvdseven  11854  gcdmndc  11877  zsupcllemstep  11878  infssuzex  11882  gcdsupex  11890  gcdsupcl  11891  gcdeq0  11910  gcdaddm  11917  rppwr  11961  uzwodc  11970  nnwosdc  11972  algfx  11984  eucalgcvga  11990  lcmmndc  11994  lcmval  11995  lcmcllem  11999  lcmledvds  12002  lcmeq0  12003  qredeq  12028  isprm3  12050  prmdc  12062  rpexp  12085  sqpweven  12107  2sqpwodd  12108  phicl2  12146  phibnd  12149  phiprmpw  12154  fermltl  12166  pythagtriplem4  12200  pythagtriplem6  12202  pythagtriplem7  12203  pythagtriplem12  12207  pythagtriplem13  12208  pythagtriplem14  12209  pythagtriplem16  12211  pclemdc  12220  pcdvdsb  12251  pc2dvds  12261  difsqpwdvds  12269  pcmpt  12273  pcmptdvds  12275  fldivp1  12278  prmpwdvds  12285  infpnlem1  12289  infpnlem2  12290  1arith  12297  ennnfonelemk  12333  ennnfonelemhom  12348  ennnfonelemrnh  12349  ennnfonelemf1  12351  ctinf  12363  ctiunctlemudc  12370  ctiunctlemf  12371  nninfdclemcl  12381  nninfdclemp1  12383  strslfvd  12435  strslfv2d  12436  strslssd  12440  lidrididd  12613  eltg3  12697  iuncld  12755  cnss2  12867  txcnp  12911  uptx  12914  xblm  13057  metss  13134  fsumcncntop  13196  rescncf  13208  dedekindeulemlu  13239  suplociccex  13243  dedekindicclemlu  13248  dedekindicc  13251  ivthdec  13262  limccnp2lem  13285  dvaddxx  13307  dvmulxx  13308  dvrecap  13317  reeff1olem  13332  lgsval  13545  lgsfvalg  13546  lgsfcl2  13547  lgscllem  13548  lgsval2lem  13551  lgsneg  13565  lgsdir2  13574  lgsdir  13576  lgsdi  13578  lgsne0  13579  lgsdirnn0  13588  lgsdinn0  13589  2sqlem6  13596  sumdc2  13680  pwle2  13878  subctctexmid  13881  nninfsellemeq  13894  exmidsbthrlem  13901