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  4377  euotd  4395  ssorduni  4634  tfisi  4734  omsinds  4769  nnpredcl  4770  sotri2  5185  sotri3  5186  unielrel  5315  funmo  5392  fnfvima  5953  resfvresima  5956  fliftfun  6002  fliftval  6006  riota5f  6065  riotass2  6067  fovcld  6193  oprssdmm  6405  funsssuppss  6498  tfrlem5  6585  tfrlemibxssdm  6598  tfrlemibfn  6599  tfrlemiex  6602  tfr1onlemsucfn  6611  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemex  6618  tfr1onlemres  6620  tfrcllemsucfn  6624  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemex  6631  tfrcllemres  6633  tfrcl  6635  rdgisucinc  6656  frecabex  6669  frecabcl  6670  nntr2  6776  ertr  6822  qliftlem  6887  th3q  6914  resixp  7015  f1dom2g  7042  dom3d  7060  domssr  7064  en1  7086  xpdom3m  7132  xpf1o  7144  phplem4dom  7163  phpm  7167  phpelm  7168  findcard  7192  finexdc  7207  fiintim  7238  fisseneq  7242  ssfirab  7244  opabfi  7247  f1dmvrnfibi  7258  iunfidisj  7260  fidcenumlemrk  7271  dcfi  7315  fdcf1  7316  2omapfi  7321  suplub2ti  7342  supelti  7343  ordiso2  7376  caseinl  7432  caseinr  7433  djudom  7434  difinfsn  7441  difinfinf  7442  ctm  7450  enumct  7456  nnnninfeq  7469  ismkvnex  7496  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  acfun  7564  exmidontriimlem2  7579  exmidontriimlem3  7580  exmidapne  7627  cc2lem  7633  cc3  7635  recexnq  7758  ltbtwnnqq  7783  addnnnq0  7817  mulnnnq0  7818  prarloclemn  7867  prarloc  7871  distrlem1prl  7950  distrlem1pru  7951  distrlem4prl  7952  distrlem4pru  7953  ltexprlemrl  7978  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  addsrpr  8113  mulsrpr  8114  map2psrprg  8173  axpre-suploclemres  8269  lemul12a  9195  lemulge11  9199  sup3exmid  9290  nngt0  9332  nn0ge0  9593  nn0ge2m1nn  9632  zletric  9693  zlelttric  9694  nn0n0n1ge2b  9730  nn0ind-raph  9768  supinfneg  10005  infsupneg  10006  infregelbex  10008  rpge0  10078  fz0fzelfz0  10545  fz0fzdiffz0  10548  ige2m2fzo  10627  elfzodifsumelfzo  10630  elfzom1elp1fzo  10631  exfzdc  10670  zsupcllemstep  10673  infssuzex  10677  qletric  10687  qlelttric  10688  rebtwn2zlemshrink  10699  frecuzrdgtcl  10864  frecuzrdg0  10865  frecuzrdgfunlem  10871  frecuzrdg0t  10874  frecuzrdgsuctlem  10875  frecfzennn  10878  seq3f1olemstep  10966  expcl2lemap  11003  leexp1a  11046  expnbnd  11116  faclbnd  11195  faclbnd6  11198  facavg  11200  fihasheqf1oi  11242  fihashf1rn  11243  fihashss  11273  fiubm  11287  seq3coll  11310  wrdsymb0  11353  wrdlenge2n0  11356  ccatsymb  11386  pfxnd  11477  pfxccat1  11490  swrdpfx  11495  pfxpfx  11496  wrd2ind  11511  pfxccatin12  11521  pfxccat3  11522  swrdccat  11523  pfxccatpfx1  11524  pfxccatpfx2  11525  swrdccatin1d  11531  pfxccatin12d  11533  resqrexlemdecn  11794  qabsor  11857  cau3lem  11897  xrmaxiflemab  12032  xrmaxadd  12046  climcn2  12094  sumeq2  12144  sumrbdclem  12163  summodclem3  12166  summodclem2a  12167  zsumdc  12170  fsumgcl  12172  fsum3  12173  isumss  12177  fsumadd  12192  fsum2dlemstep  12220  fisum0diag2  12233  fsummulc2  12234  modfsummodlemstep  12243  fsumabs  12251  fsumrelem  12257  fsumiun  12263  isumshft  12276  mertenslem2  12322  prodeq2  12343  prodrbdclem  12357  prodmodclem3  12361  prodmodclem2a  12362  zproddc  12365  fprodseq  12369  fprodmul  12377  fprodconst  12406  fprodap0  12407  fprod2dlemstep  12408  fprodrec  12415  fprodsplit1f  12420  fprodap0f  12422  fprodle  12426  sin02gt0  12550  efieq1re  12558  p1modz1  12580  dvdsleabs2  12632  4dvdseven  12703  bitsfzo  12741  bitsinv1lem  12747  gcdeq0  12773  rppwr  12824  uzwodc  12833  algfx  12849  eucalgcvga  12855  lcmmndc  12859  lcmeq0  12868  qredeq  12893  isprm3  12915  rpexp  12951  sqpweven  12974  2sqpwodd  12975  phicl2  13015  phibnd  13018  phiprmpw  13023  fermltl  13035  pythagtriplem4  13070  pythagtriplem6  13072  pythagtriplem7  13073  pythagtriplem12  13077  pythagtriplem13  13078  pythagtriplem14  13079  pythagtriplem16  13081  pcdvdsb  13122  pc2dvds  13132  difsqpwdvds  13140  pcmpt  13145  pcmptdvds  13147  fldivp1  13150  prmpwdvds  13157  infpnlem1  13161  1arith  13169  4sqlem11  13203  prmlem1  13245  prmlem2  13257  ballotfilemfp1  13283  ballotfilemic  13302  ennnfonelemk  13343  ennnfonelemhom  13358  ennnfonelemrnh  13359  ennnfonelemf1  13361  ctinf  13373  ctiunctlemudc  13380  ctiunctlemf  13381  nninfdclemp1  13393  strslfvd  13446  strslfv2d  13447  strslssd  13451  imasival  13680  imasbas  13681  imasplusg  13682  imasaddfnlemg  13688  imasaddvallemg  13689  qusaddvallemg  13707  qusaddflemg  13708  qusaddval  13709  qusaddf  13710  qusmulval  13711  qusmulf  13712  lidrididd  13755  gzsumfzval  13764  sgrpidmndm  13786  qusgrp2  13969  mulgnegnn  13988  eqgen  14083  rinvmod  14197  gzsumconst  14227  gsump1  14241  gsummptfidmadd  14245  qusrng  14341  srgdilem  14357  ringdilem  14400  qusring2  14455  lssintclm  14805  mplsubgfilemm  15180  eltg3  15249  iuncld  15307  cnss2  15419  txcnp  15463  uptx  15466  xblm  15609  metss  15686  fsumcncntop  15759  rescncf  15773  dedekindeulemlu  15813  suplociccex  15817  dedekindicclemlu  15822  dedekindicc  15825  ivthdec  15836  limccnp2lem  15868  dvaddxx  15895  dvmulxx  15896  dvrecap  15905  reeff1olem  15963  ppiqwordi  16229  ppiqeq0  16241  ppiqub  16254  perfectlem2  16261  lgsval  16289  lgsfvalg  16290  lgsfcl2  16291  lgscllem  16292  lgsval2lem  16295  lgsneg  16309  lgsdir2  16318  lgsdir  16320  lgsdi  16322  lgsne0  16323  lgsdirnn0  16332  lgsdinn0  16333  gausslemma2dlem0c  16336  m1lgs  16370  2lgslem1  16376  2lgs  16389  2lgsoddprm  16398  2sqlem6  16405  incistruhgr  16497  upgredg  16551  uhgr2edg  16613  usgriedgdomord  16632  wlkpropg  16731  wlkvtxeledgg  16751  wlk2f  16758  clwwlknonccat  16840  clwwlknonex2lem2  16845  eupth2lem3lem4fi  16880  eupth2lem3lem7fi  16881  dichmul0orlem3  16921  sumdc2  16993  pwle2  17194  subctctexmid  17196  nninfsellemeq  17223  nnnninfex  17231  exmidsbthrlem  17233  cndcap  17276