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  656  jcnd  658  annimdc  945  pm4.55dc  946  orandc  947  dn1dc  968  syl2an23an  1335  xordidc  1443  nfimd  1633  exlimd2  1643  elex22  2818  elex2  2819  spcimdv  2890  spcimedv  2892  spcedv  2895  rspcdva  2915  elabd  2951  spsbcd  3044  opth  4329  euotd  4347  ssorduni  4585  tfisi  4685  omsinds  4720  nnpredcl  4721  sotri2  5134  sotri3  5135  unielrel  5264  funmo  5341  fnfvima  5888  resfvresima  5890  fliftfun  5936  fliftval  5940  riota5f  5997  riotass2  5999  fovcld  6125  oprssdmm  6333  tfrlem5  6479  tfrlemibxssdm  6492  tfrlemibfn  6493  tfrlemiex  6496  tfr1onlemsucfn  6505  tfr1onlemsucaccv  6506  tfr1onlembxssdm  6508  tfr1onlembfn  6509  tfr1onlemex  6512  tfr1onlemres  6514  tfrcllemsucfn  6518  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  tfrcllembfn  6522  tfrcllemex  6525  tfrcllemres  6527  tfrcl  6529  rdgisucinc  6550  frecabex  6563  frecabcl  6564  nntr2  6670  ertr  6716  qliftlem  6781  th3q  6808  resixp  6901  f1dom2g  6928  dom3d  6946  domssr  6950  en1  6972  xpdom3m  7017  xpf1o  7029  phplem4dom  7047  phpm  7051  phpelm  7052  findcard  7076  finexdc  7091  fiintim  7122  fisseneq  7126  ssfirab  7128  opabfi  7131  f1dmvrnfibi  7142  iunfidisj  7144  fidcenumlemrk  7152  dcfi  7179  suplub2ti  7199  supelti  7200  ordiso2  7233  caseinl  7289  caseinr  7290  djudom  7291  difinfsn  7298  difinfinf  7299  ctm  7307  enumct  7313  nnnninfeq  7326  ismkvnex  7353  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  acfun  7421  exmidontriimlem2  7436  exmidontriimlem3  7437  exmidapne  7478  cc2lem  7484  cc3  7486  recexnq  7609  ltbtwnnqq  7634  addnnnq0  7668  mulnnnq0  7669  prarloclemn  7718  prarloc  7722  distrlem1prl  7801  distrlem1pru  7802  distrlem4prl  7803  distrlem4pru  7804  ltexprlemrl  7829  cauappcvgprlemladdru  7875  cauappcvgprlemladdrl  7876  addsrpr  7964  mulsrpr  7965  map2psrprg  8024  axpre-suploclemres  8120  lemul12a  9041  lemulge11  9045  sup3exmid  9136  nngt0  9167  nn0ge0  9426  nn0ge2m1nn  9461  zletric  9522  zlelttric  9523  nn0n0n1ge2b  9558  nn0ind-raph  9596  supinfneg  9828  infsupneg  9829  infregelbex  9831  rpge0  9900  fz0fzelfz0  10361  fz0fzdiffz0  10364  ige2m2fzo  10442  elfzodifsumelfzo  10445  elfzom1elp1fzo  10446  exfzdc  10485  zsupcllemstep  10488  infssuzex  10492  qletric  10500  qlelttric  10501  rebtwn2zlemshrink  10512  frecuzrdgtcl  10673  frecuzrdg0  10674  frecuzrdgfunlem  10680  frecuzrdg0t  10683  frecuzrdgsuctlem  10684  frecfzennn  10687  seq3f1olemstep  10775  expcl2lemap  10812  leexp1a  10855  expnbnd  10924  faclbnd  11002  faclbnd6  11005  facavg  11007  fihasheqf1oi  11048  fihashf1rn  11049  fihashss  11079  fiubm  11091  seq3coll  11105  wrdsymb0  11145  wrdlenge2n0  11148  ccatsymb  11178  pfxnd  11269  pfxccat1  11282  swrdpfx  11287  pfxpfx  11288  wrd2ind  11303  pfxccatin12  11313  pfxccat3  11314  swrdccat  11315  pfxccatpfx1  11316  pfxccatpfx2  11317  swrdccatin1d  11323  pfxccatin12d  11325  resqrexlemdecn  11572  qabsor  11635  cau3lem  11674  xrmaxiflemab  11807  xrmaxadd  11821  climcn2  11869  sumeq2  11919  sumrbdclem  11937  summodclem3  11940  summodclem2a  11941  zsumdc  11944  fsumgcl  11946  fsum3  11947  isumss  11951  fsumadd  11966  fsum2dlemstep  11994  fisum0diag2  12007  fsummulc2  12008  modfsummodlemstep  12017  fsumabs  12025  fsumrelem  12031  fsumiun  12037  isumshft  12050  mertenslem2  12096  prodeq2  12117  prodrbdclem  12131  prodmodclem3  12135  prodmodclem2a  12136  zproddc  12139  fprodseq  12143  fprodmul  12151  fprodconst  12180  fprodap0  12181  fprod2dlemstep  12182  fprodrec  12189  fprodsplit1f  12194  fprodap0f  12196  fprodle  12200  sin02gt0  12324  efieq1re  12332  p1modz1  12354  dvdsleabs2  12406  4dvdseven  12477  bitsfzo  12515  bitsinv1lem  12521  gcdeq0  12547  rppwr  12598  uzwodc  12607  algfx  12623  eucalgcvga  12629  lcmmndc  12633  lcmeq0  12642  qredeq  12667  isprm3  12689  rpexp  12724  sqpweven  12746  2sqpwodd  12747  phicl2  12785  phibnd  12788  phiprmpw  12793  fermltl  12805  pythagtriplem4  12840  pythagtriplem6  12842  pythagtriplem7  12843  pythagtriplem12  12847  pythagtriplem13  12848  pythagtriplem14  12849  pythagtriplem16  12851  pcdvdsb  12892  pc2dvds  12902  difsqpwdvds  12910  pcmpt  12915  pcmptdvds  12917  fldivp1  12920  prmpwdvds  12927  infpnlem1  12931  1arith  12939  4sqlem11  12973  ennnfonelemk  13020  ennnfonelemhom  13035  ennnfonelemrnh  13036  ennnfonelemf1  13038  ctinf  13050  ctiunctlemudc  13057  ctiunctlemf  13058  nninfdclemp1  13070  strslfvd  13123  strslfv2d  13124  strslssd  13128  imasival  13388  imasbas  13389  imasplusg  13390  imasaddfnlemg  13396  imasaddvallemg  13397  qusaddvallemg  13415  qusaddflemg  13416  qusaddval  13417  qusaddf  13418  qusmulval  13419  qusmulf  13420  lidrididd  13464  gsumfzval  13473  sgrpidmndm  13502  gsumfzz  13577  qusgrp2  13699  mulgnegnn  13718  eqgen  13813  rinvmod  13895  gsumfzconst  13927  qusrng  13970  srgdilem  13981  ringdilem  14024  qusring2  14078  lssintclm  14397  gsumfzfsumlemm  14600  mplsubgfilemm  14711  eltg3  14780  iuncld  14838  cnss2  14950  txcnp  14994  uptx  14997  xblm  15140  metss  15217  fsumcncntop  15290  rescncf  15304  dedekindeulemlu  15344  suplociccex  15348  dedekindicclemlu  15353  dedekindicc  15356  ivthdec  15367  limccnp2lem  15399  dvaddxx  15426  dvmulxx  15427  dvrecap  15436  reeff1olem  15494  perfectlem2  15723  lgsval  15732  lgsfvalg  15733  lgsfcl2  15734  lgscllem  15735  lgsval2lem  15738  lgsneg  15752  lgsdir2  15761  lgsdir  15763  lgsdi  15765  lgsne0  15766  lgsdirnn0  15775  lgsdinn0  15776  gausslemma2dlem0c  15779  m1lgs  15813  2lgslem1  15819  2lgs  15832  2lgsoddprm  15841  2sqlem6  15848  incistruhgr  15940  upgredg  15994  uhgr2edg  16056  usgriedgdomord  16075  wlkpropg  16174  wlkvtxeledgg  16194  wlk2f  16201  clwwlknonccat  16283  clwwlknonex2lem2  16288  sumdc2  16395  pwle2  16599  subctctexmid  16601  nninfsellemeq  16616  nnnninfex  16624  exmidsbthrlem  16626  cndcap  16663