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  124  2thd  175  jca  306  syl2anc  411  jc  651  jcnd  653  annimdc  939  pm4.55dc  940  orandc  941  dn1dc  962  syl2an23an  1310  xordidc  1410  nfimd  1596  exlimd2  1606  elex22  2775  elex2  2776  spcimdv  2844  spcimedv  2846  spcedv  2849  rspcdva  2869  elabd  2905  spsbcd  2998  opth  4266  euotd  4283  ssorduni  4519  tfisi  4619  omsinds  4654  nnpredcl  4655  sotri2  5063  sotri3  5064  unielrel  5193  funmo  5269  fnfvima  5793  fliftfun  5839  fliftval  5843  riota5f  5898  riotass2  5900  fovcld  6023  oprssdmm  6224  tfrlem5  6367  tfrlemibxssdm  6380  tfrlemibfn  6381  tfrlemiex  6384  tfr1onlemsucfn  6393  tfr1onlemsucaccv  6394  tfr1onlembxssdm  6396  tfr1onlembfn  6397  tfr1onlemex  6400  tfr1onlemres  6402  tfrcllemsucfn  6406  tfrcllemsucaccv  6407  tfrcllembxssdm  6409  tfrcllembfn  6410  tfrcllemex  6413  tfrcllemres  6415  tfrcl  6417  rdgisucinc  6438  frecabex  6451  frecabcl  6452  nntr2  6556  ertr  6602  qliftlem  6667  th3q  6694  resixp  6787  f1dom2g  6810  dom3d  6828  en1  6853  xpdom3m  6888  xpf1o  6900  phplem4dom  6918  phpm  6921  phpelm  6922  findcard  6944  finexdc  6958  fiintim  6985  fisseneq  6988  ssfirab  6990  opabfi  6992  f1dmvrnfibi  7003  iunfidisj  7005  fidcenumlemrk  7013  dcfi  7040  suplub2ti  7060  supelti  7061  ordiso2  7094  caseinl  7150  caseinr  7151  djudom  7152  difinfsn  7159  difinfinf  7160  ctm  7168  enumct  7174  nnnninfeq  7187  ismkvnex  7214  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  acfun  7267  exmidontriimlem2  7282  exmidontriimlem3  7283  exmidapne  7320  cc2lem  7326  cc3  7328  recexnq  7450  ltbtwnnqq  7475  addnnnq0  7509  mulnnnq0  7510  prarloclemn  7559  prarloc  7563  distrlem1prl  7642  distrlem1pru  7643  distrlem4prl  7644  distrlem4pru  7645  ltexprlemrl  7670  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  addsrpr  7805  mulsrpr  7806  map2psrprg  7865  axpre-suploclemres  7961  lemul12a  8881  lemulge11  8885  sup3exmid  8976  nngt0  9007  nn0ge0  9265  nn0ge2m1nn  9300  zletric  9361  zlelttric  9362  nn0n0n1ge2b  9396  nn0ind-raph  9434  supinfneg  9660  infsupneg  9661  infregelbex  9663  rpge0  9732  fz0fzelfz0  10193  fz0fzdiffz0  10196  ige2m2fzo  10265  elfzodifsumelfzo  10268  elfzom1elp1fzo  10269  exfzdc  10307  qletric  10311  qlelttric  10312  rebtwn2zlemshrink  10322  frecuzrdgtcl  10483  frecuzrdg0  10484  frecuzrdgfunlem  10490  frecuzrdg0t  10493  frecuzrdgsuctlem  10494  frecfzennn  10497  seq3f1olemstep  10585  expcl2lemap  10622  leexp1a  10665  expnbnd  10734  faclbnd  10812  faclbnd6  10815  facavg  10817  fihasheqf1oi  10858  fihashf1rn  10859  fihashss  10887  fiubm  10899  seq3coll  10913  wrdsymb0  10946  wrdlenge2n0  10949  resqrexlemdecn  11156  qabsor  11219  cau3lem  11258  xrmaxiflemab  11390  xrmaxadd  11404  climcn2  11452  sumeq2  11502  sumrbdclem  11520  summodclem3  11523  summodclem2a  11524  zsumdc  11527  fsumgcl  11529  fsum3  11530  isumss  11534  fsumadd  11549  fsum2dlemstep  11577  fisum0diag2  11590  fsummulc2  11591  modfsummodlemstep  11600  fsumabs  11608  fsumrelem  11614  fsumiun  11620  isumshft  11633  mertenslem2  11679  prodeq2  11700  prodrbdclem  11714  prodmodclem3  11718  prodmodclem2a  11719  zproddc  11722  fprodseq  11726  fprodmul  11734  fprodconst  11763  fprodap0  11764  fprod2dlemstep  11765  fprodrec  11772  fprodsplit1f  11777  fprodap0f  11779  fprodle  11783  sin02gt0  11907  efieq1re  11915  p1modz1  11937  dvdsleabs2  11988  4dvdseven  12058  zsupcllemstep  12082  infssuzex  12086  gcdeq0  12114  rppwr  12165  uzwodc  12174  algfx  12190  eucalgcvga  12196  lcmmndc  12200  lcmeq0  12209  qredeq  12234  isprm3  12256  rpexp  12291  sqpweven  12313  2sqpwodd  12314  phicl2  12352  phibnd  12355  phiprmpw  12360  fermltl  12372  pythagtriplem4  12406  pythagtriplem6  12408  pythagtriplem7  12409  pythagtriplem12  12413  pythagtriplem13  12414  pythagtriplem14  12415  pythagtriplem16  12417  pcdvdsb  12458  pc2dvds  12468  difsqpwdvds  12476  pcmpt  12481  pcmptdvds  12483  fldivp1  12486  prmpwdvds  12493  infpnlem1  12497  1arith  12505  4sqlem11  12539  ennnfonelemk  12557  ennnfonelemhom  12572  ennnfonelemrnh  12573  ennnfonelemf1  12575  ctinf  12587  ctiunctlemudc  12594  ctiunctlemf  12595  nninfdclemp1  12607  strslfvd  12660  strslfv2d  12661  strslssd  12665  imasival  12889  imasbas  12890  imasplusg  12891  imasaddfnlemg  12897  imasaddvallemg  12898  qusaddvallemg  12916  qusaddflemg  12917  qusaddval  12918  qusaddf  12919  qusmulval  12920  qusmulf  12921  lidrididd  12965  gsumfzval  12974  sgrpidmndm  13001  gsumfzz  13067  qusgrp2  13183  mulgnegnn  13202  eqgen  13297  rinvmod  13379  gsumfzconst  13411  qusrng  13454  srgdilem  13465  ringdilem  13508  qusring2  13562  lssintclm  13880  gsumfzfsumlemm  14075  eltg3  14225  iuncld  14283  cnss2  14395  txcnp  14439  uptx  14442  xblm  14585  metss  14662  fsumcncntop  14724  rescncf  14736  dedekindeulemlu  14775  suplociccex  14779  dedekindicclemlu  14784  dedekindicc  14787  ivthdec  14798  limccnp2lem  14830  dvaddxx  14852  dvmulxx  14853  dvrecap  14862  reeff1olem  14906  lgsval  15120  lgsfvalg  15121  lgsfcl2  15122  lgscllem  15123  lgsval2lem  15126  lgsneg  15140  lgsdir2  15149  lgsdir  15151  lgsdi  15153  lgsne0  15154  lgsdirnn0  15163  lgsdinn0  15164  gausslemma2dlem0c  15167  m1lgs  15192  2sqlem6  15207  sumdc2  15291  pwle2  15489  subctctexmid  15491  nninfsellemeq  15504  exmidsbthrlem  15512  cndcap  15549