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  1311  xordidc  1418  nfimd  1607  exlimd2  1617  elex22  2786  elex2  2787  spcimdv  2856  spcimedv  2858  spcedv  2861  rspcdva  2881  elabd  2917  spsbcd  3010  opth  4280  euotd  4298  ssorduni  4534  tfisi  4634  omsinds  4669  nnpredcl  4670  sotri2  5079  sotri3  5080  unielrel  5209  funmo  5285  fnfvima  5818  fliftfun  5864  fliftval  5868  riota5f  5923  riotass2  5925  fovcld  6049  oprssdmm  6256  tfrlem5  6399  tfrlemibxssdm  6412  tfrlemibfn  6413  tfrlemiex  6416  tfr1onlemsucfn  6425  tfr1onlemsucaccv  6426  tfr1onlembxssdm  6428  tfr1onlembfn  6429  tfr1onlemex  6432  tfr1onlemres  6434  tfrcllemsucfn  6438  tfrcllemsucaccv  6439  tfrcllembxssdm  6441  tfrcllembfn  6442  tfrcllemex  6445  tfrcllemres  6447  tfrcl  6449  rdgisucinc  6470  frecabex  6483  frecabcl  6484  nntr2  6588  ertr  6634  qliftlem  6699  th3q  6726  resixp  6819  f1dom2g  6846  dom3d  6864  domssr  6868  en1  6890  xpdom3m  6928  xpf1o  6940  phplem4dom  6958  phpm  6961  phpelm  6962  findcard  6984  finexdc  6998  fiintim  7027  fisseneq  7030  ssfirab  7032  opabfi  7034  f1dmvrnfibi  7045  iunfidisj  7047  fidcenumlemrk  7055  dcfi  7082  suplub2ti  7102  supelti  7103  ordiso2  7136  caseinl  7192  caseinr  7193  djudom  7194  difinfsn  7201  difinfinf  7202  ctm  7210  enumct  7216  nnnninfeq  7229  ismkvnex  7256  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  acfun  7318  exmidontriimlem2  7333  exmidontriimlem3  7334  exmidapne  7371  cc2lem  7377  cc3  7379  recexnq  7502  ltbtwnnqq  7527  addnnnq0  7561  mulnnnq0  7562  prarloclemn  7611  prarloc  7615  distrlem1prl  7694  distrlem1pru  7695  distrlem4prl  7696  distrlem4pru  7697  ltexprlemrl  7722  cauappcvgprlemladdru  7768  cauappcvgprlemladdrl  7769  addsrpr  7857  mulsrpr  7858  map2psrprg  7917  axpre-suploclemres  8013  lemul12a  8934  lemulge11  8938  sup3exmid  9029  nngt0  9060  nn0ge0  9319  nn0ge2m1nn  9354  zletric  9415  zlelttric  9416  nn0n0n1ge2b  9451  nn0ind-raph  9489  supinfneg  9715  infsupneg  9716  infregelbex  9718  rpge0  9787  fz0fzelfz0  10248  fz0fzdiffz0  10251  ige2m2fzo  10325  elfzodifsumelfzo  10328  elfzom1elp1fzo  10329  exfzdc  10367  zsupcllemstep  10370  infssuzex  10374  qletric  10382  qlelttric  10383  rebtwn2zlemshrink  10394  frecuzrdgtcl  10555  frecuzrdg0  10556  frecuzrdgfunlem  10562  frecuzrdg0t  10565  frecuzrdgsuctlem  10566  frecfzennn  10569  seq3f1olemstep  10657  expcl2lemap  10694  leexp1a  10737  expnbnd  10806  faclbnd  10884  faclbnd6  10887  facavg  10889  fihasheqf1oi  10930  fihashf1rn  10931  fihashss  10959  fiubm  10971  seq3coll  10985  wrdsymb0  11024  wrdlenge2n0  11027  ccatsymb  11056  resqrexlemdecn  11294  qabsor  11357  cau3lem  11396  xrmaxiflemab  11529  xrmaxadd  11543  climcn2  11591  sumeq2  11641  sumrbdclem  11659  summodclem3  11662  summodclem2a  11663  zsumdc  11666  fsumgcl  11668  fsum3  11669  isumss  11673  fsumadd  11688  fsum2dlemstep  11716  fisum0diag2  11729  fsummulc2  11730  modfsummodlemstep  11739  fsumabs  11747  fsumrelem  11753  fsumiun  11759  isumshft  11772  mertenslem2  11818  prodeq2  11839  prodrbdclem  11853  prodmodclem3  11857  prodmodclem2a  11858  zproddc  11861  fprodseq  11865  fprodmul  11873  fprodconst  11902  fprodap0  11903  fprod2dlemstep  11904  fprodrec  11911  fprodsplit1f  11916  fprodap0f  11918  fprodle  11922  sin02gt0  12046  efieq1re  12054  p1modz1  12076  dvdsleabs2  12128  4dvdseven  12199  bitsfzo  12237  bitsinv1lem  12243  gcdeq0  12269  rppwr  12320  uzwodc  12329  algfx  12345  eucalgcvga  12351  lcmmndc  12355  lcmeq0  12364  qredeq  12389  isprm3  12411  rpexp  12446  sqpweven  12468  2sqpwodd  12469  phicl2  12507  phibnd  12510  phiprmpw  12515  fermltl  12527  pythagtriplem4  12562  pythagtriplem6  12564  pythagtriplem7  12565  pythagtriplem12  12569  pythagtriplem13  12570  pythagtriplem14  12571  pythagtriplem16  12573  pcdvdsb  12614  pc2dvds  12624  difsqpwdvds  12632  pcmpt  12637  pcmptdvds  12639  fldivp1  12642  prmpwdvds  12649  infpnlem1  12653  1arith  12661  4sqlem11  12695  ennnfonelemk  12742  ennnfonelemhom  12757  ennnfonelemrnh  12758  ennnfonelemf1  12760  ctinf  12772  ctiunctlemudc  12779  ctiunctlemf  12780  nninfdclemp1  12792  strslfvd  12845  strslfv2d  12846  strslssd  12850  imasival  13109  imasbas  13110  imasplusg  13111  imasaddfnlemg  13117  imasaddvallemg  13118  qusaddvallemg  13136  qusaddflemg  13137  qusaddval  13138  qusaddf  13139  qusmulval  13140  qusmulf  13141  lidrididd  13185  gsumfzval  13194  sgrpidmndm  13223  gsumfzz  13298  qusgrp2  13420  mulgnegnn  13439  eqgen  13534  rinvmod  13616  gsumfzconst  13648  qusrng  13691  srgdilem  13702  ringdilem  13745  qusring2  13799  lssintclm  14117  gsumfzfsumlemm  14320  mplsubgfilemm  14431  eltg3  14500  iuncld  14558  cnss2  14670  txcnp  14714  uptx  14717  xblm  14860  metss  14937  fsumcncntop  15010  rescncf  15024  dedekindeulemlu  15064  suplociccex  15068  dedekindicclemlu  15073  dedekindicc  15076  ivthdec  15087  limccnp2lem  15119  dvaddxx  15146  dvmulxx  15147  dvrecap  15156  reeff1olem  15214  perfectlem2  15443  lgsval  15452  lgsfvalg  15453  lgsfcl2  15454  lgscllem  15455  lgsval2lem  15458  lgsneg  15472  lgsdir2  15481  lgsdir  15483  lgsdi  15485  lgsne0  15486  lgsdirnn0  15495  lgsdinn0  15496  gausslemma2dlem0c  15499  m1lgs  15533  2lgslem1  15539  2lgs  15552  2lgsoddprm  15561  2sqlem6  15568  sumdc2  15697  pwle2  15897  subctctexmid  15899  nninfsellemeq  15913  nnnninfex  15921  exmidsbthrlem  15923  cndcap  15960