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	|- ( ph -> ps )
sylc.2	|- ( ph -> ch )
sylc.3	|- ( ps -> ( ch -> th ) )

Assertion

Ref	Expression
sylc	|- ( ph -> th )

Proof of Theorem sylc

Step	Hyp	Ref	Expression
1		sylc.1	. . 3 |- ( ph -> ps )
2		sylc.2	. . 3 |- ( ph -> ch )
3		sylc.3	. . 3 |- ( ps -> ( ch -> th ) )
4	1, 2, 3	syl2im 38	. 2 |- ( ph -> ( ph -> th ) )
5	4	pm2.43i 49	1 |- ( ph -> th )

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:  syl3c  63  mpsyl  65  imp  124  2thd  175  jca  306  syl2anc  415  jc  660  jcnd  662  annimdc  950  pm4.55dc  951  orandc  952  dn1dc  973  syl2an23an  1340  xordidc  1448  nfimd  1638  exlimd2  1648  elex22  2837  elex2  2838  spcimdv  2909  spcimedv  2911  spcedv  2914  rspcdva  2934  elabd  2971  spsbcd  3064  ifeqeqxdc  3687  opth  4379  euotd  4397  ssorduni  4636  tfisi  4736  omsinds  4771  nnpredcl  4772  sotri2  5188  sotri3  5189  unielrel  5318  funmo  5395  fnfvima  5956  resfvresima  5959  fliftfun  6005  fliftval  6009  riota5f  6068  riotass2  6070  fovcld  6196  oprssdmm  6409  funsssuppss  6502  tfrlem5  6590  tfrlemibxssdm  6603  tfrlemibfn  6604  tfrlemiex  6607  tfr1onlemsucfn  6616  tfr1onlemsucaccv  6617  tfr1onlembxssdm  6619  tfr1onlembfn  6620  tfr1onlemex  6623  tfr1onlemres  6625  tfrcllemsucfn  6629  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllembfn  6633  tfrcllemex  6636  tfrcllemres  6638  tfrcl  6640  rdgisucinc  6661  frecabex  6674  frecabcl  6675  nntr2  6781  ertr  6827  qliftlem  6892  th3q  6919  resixp  7021  f1dom2g  7048  dom3d  7066  domssr  7070  en1  7092  xpdom3m  7138  xpf1o  7150  phplem4dom  7169  phpm  7173  phpelm  7174  findcard  7198  finexdc  7213  fiintim  7244  fisseneq  7248  ssfirab  7250  opabfi  7253  f1dmvrnfibi  7264  iunfidisj  7266  fidcenumlemrk  7278  dcfi  7320  fdcf1  7321  2omapfi  7326  suplub2ti  7347  supelti  7348  ordiso2  7381  caseinl  7437  caseinr  7438  djudom  7439  difinfsn  7446  difinfinf  7447  ctm  7455  enumct  7461  nnnninfeq  7474  ismkvnex  7501  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  acfun  7569  exmidontriimlem2  7584  exmidontriimlem3  7585  exmidapne  7632  cc2lem  7638  cc3  7640  recexnq  7763  ltbtwnnqq  7788  addnnnq0  7822  mulnnnq0  7823  prarloclemn  7872  prarloc  7876  distrlem1prl  7955  distrlem1pru  7956  distrlem4prl  7957  distrlem4pru  7958  ltexprlemrl  7983  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  addsrpr  8118  mulsrpr  8119  map2psrprg  8178  axpre-suploclemres  8274  lemul12a  9200  lemulge11  9204  sup3exmid  9295  nngt0  9338  nn0ge0  9599  nn0ge2m1nn  9636  zletric  9697  zlelttric  9698  nn0n0n1ge2b  9734  nn0ind-raph  9773  supinfneg  10010  infsupneg  10011  infregelbex  10013  rpge0  10083  fz0fzelfz0  10550  fz0fzdiffz0  10553  ige2m2fzo  10632  elfzodifsumelfzo  10635  elfzom1elp1fzo  10636  exfzdc  10675  zsupcllemstep  10678  infssuzex  10682  qletric  10692  qlelttric  10693  rebtwn2zlemshrink  10704  frecuzrdgtcl  10869  frecuzrdg0  10870  frecuzrdgfunlem  10876  frecuzrdg0t  10879  frecuzrdgsuctlem  10880  frecfzennn  10883  seq3f1olemstep  10971  expcl2lemap  11008  leexp1a  11051  expnbnd  11121  faclbnd  11200  faclbnd6  11203  facavg  11205  fihasheqf1oi  11247  fihashf1rn  11248  fihashss  11278  fiubm  11292  seq3coll  11315  wrdsymb0  11358  wrdlenge2n0  11361  ccatsymb  11391  pfxnd  11482  pfxccat1  11495  swrdpfx  11500  pfxpfx  11501  wrd2ind  11516  pfxccatin12  11526  pfxccat3  11527  swrdccat  11528  pfxccatpfx1  11529  pfxccatpfx2  11530  swrdccatin1d  11536  pfxccatin12d  11538  resqrexlemdecn  11799  qabsor  11862  cau3lem  11902  xrmaxiflemab  12037  xrmaxadd  12051  climcn2  12099  sumeq2  12149  sumrbdclem  12168  summodclem3  12171  summodclem2a  12172  zsumdc  12175  fsumgcl  12177  fsum3  12178  isumss  12182  fsumadd  12197  fsum2dlemstep  12225  fisum0diag2  12238  fsummulc2  12239  modfsummodlemstep  12248  fsumabs  12256  fsumrelem  12262  fsumiun  12268  isumshft  12281  mertenslem2  12327  prodeq2  12348  prodrbdclem  12362  prodmodclem3  12366  prodmodclem2a  12367  zproddc  12370  fprodseq  12374  fprodmul  12382  fprodconst  12411  fprodap0  12412  fprod2dlemstep  12413  fprodrec  12420  fprodsplit1f  12425  fprodap0f  12427  fprodle  12431  sin02gt0  12555  efieq1re  12563  p1modz1  12585  dvdsleabs2  12637  4dvdseven  12708  bitsfzo  12746  bitsinv1lem  12752  gcdeq0  12778  rppwr  12829  uzwodc  12838  algfx  12854  eucalgcvga  12860  lcmmndc  12864  lcmeq0  12873  qredeq  12898  isprm3  12920  rpexp  12956  sqpweven  12979  2sqpwodd  12980  phicl2  13020  phibnd  13023  phiprmpw  13028  fermltl  13040  pythagtriplem4  13075  pythagtriplem6  13077  pythagtriplem7  13078  pythagtriplem12  13082  pythagtriplem13  13083  pythagtriplem14  13084  pythagtriplem16  13086  pcdvdsb  13127  pc2dvds  13137  difsqpwdvds  13145  pcmpt  13150  pcmptdvds  13152  fldivp1  13155  prmpwdvds  13162  infpnlem1  13166  1arith  13174  4sqlem11  13208  prmlem1  13250  prmlem2  13262  ballotfilemfp1  13288  ballotfilemic  13307  ennnfonelemk  13348  ennnfonelemhom  13363  ennnfonelemrnh  13364  ennnfonelemf1  13366  ctinf  13378  ctiunctlemudc  13385  ctiunctlemf  13386  nninfdclemp1  13398  strslfvd  13451  strslfv2d  13452  strslssd  13456  imasival  13685  imasbas  13686  imasplusg  13687  imasaddfnlemg  13693  imasaddvallemg  13694  qusaddvallemg  13712  qusaddflemg  13713  qusaddval  13714  qusaddf  13715  qusmulval  13716  qusmulf  13717  lidrididd  13760  gzsumfzval  13769  sgrpidmndm  13791  qusgrp2  13974  mulgnegnn  13993  eqgen  14088  rinvmod  14202  gzsumconst  14232  gsump1  14246  gsummptfidmadd  14250  gsummptfidmsplit  14253  gsumresfi  14262  qusrng  14363  srgdilem  14379  ringdilem  14422  qusring2  14479  lssintclm  14829  psrbagmax  15183  mplsubgfilemm  15231  eltg3  15300  iuncld  15358  cnss2  15470  txcnp  15514  uptx  15517  xblm  15660  metss  15737  fsumcncntop  15810  rescncf  15824  dedekindeulemlu  15864  suplociccex  15868  dedekindicclemlu  15873  dedekindicc  15876  ivthdec  15887  limccnp2lem  15919  dvaddxx  15946  dvmulxx  15947  dvrecap  15956  reeff1olem  16014  ppiqwordi  16285  ppiqeq0  16297  ppiqub  16310  perfectlem2  16317  lgsval  16345  lgsfvalg  16346  lgsfcl2  16347  lgscllem  16348  lgsval2lem  16351  lgsneg  16365  lgsdir2  16374  lgsdir  16376  lgsdi  16378  lgsne0  16379  lgsdirnn0  16388  lgsdinn0  16389  gausslemma2dlem0c  16392  m1lgs  16426  2lgslem1  16432  2lgs  16445  2lgsoddprm  16454  2sqlem6  16461  incistruhgr  16553  upgredg  16607  uhgr2edg  16669  usgriedgdomord  16688  wlkpropg  16787  wlkvtxeledgg  16807  wlk2f  16814  clwwlknonccat  16896  clwwlknonex2lem2  16901  eupth2lem3lem4fi  16936  eupth2lem3lem7fi  16937  dichmul0orlem3  16977  sumdc2  17049  pwle2  17250  subctctexmid  17252  nninfsellemeq  17280  nnnninfex  17288  exmidsbthrlem  17290  cndcap  17333