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  654  jcnd  656  annimdc  943  pm4.55dc  944  orandc  945  dn1dc  966  syl2an23an  1333  xordidc  1441  nfimd  1631  exlimd2  1641  elex22  2815  elex2  2816  spcimdv  2887  spcimedv  2889  spcedv  2892  rspcdva  2912  elabd  2948  spsbcd  3041  opth  4322  euotd  4340  ssorduni  4578  tfisi  4678  omsinds  4713  nnpredcl  4714  sotri2  5125  sotri3  5126  unielrel  5255  funmo  5332  fnfvima  5873  fliftfun  5919  fliftval  5923  riota5f  5980  riotass2  5982  fovcld  6108  oprssdmm  6315  tfrlem5  6458  tfrlemibxssdm  6471  tfrlemibfn  6472  tfrlemiex  6475  tfr1onlemsucfn  6484  tfr1onlemsucaccv  6485  tfr1onlembxssdm  6487  tfr1onlembfn  6488  tfr1onlemex  6491  tfr1onlemres  6493  tfrcllemsucfn  6497  tfrcllemsucaccv  6498  tfrcllembxssdm  6500  tfrcllembfn  6501  tfrcllemex  6504  tfrcllemres  6506  tfrcl  6508  rdgisucinc  6529  frecabex  6542  frecabcl  6543  nntr2  6647  ertr  6693  qliftlem  6758  th3q  6785  resixp  6878  f1dom2g  6905  dom3d  6923  domssr  6927  en1  6949  xpdom3m  6989  xpf1o  7001  phplem4dom  7019  phpm  7023  phpelm  7024  findcard  7046  finexdc  7060  fiintim  7089  fisseneq  7092  ssfirab  7094  opabfi  7096  f1dmvrnfibi  7107  iunfidisj  7109  fidcenumlemrk  7117  dcfi  7144  suplub2ti  7164  supelti  7165  ordiso2  7198  caseinl  7254  caseinr  7255  djudom  7256  difinfsn  7263  difinfinf  7264  ctm  7272  enumct  7278  nnnninfeq  7291  ismkvnex  7318  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  acfun  7385  exmidontriimlem2  7400  exmidontriimlem3  7401  exmidapne  7442  cc2lem  7448  cc3  7450  recexnq  7573  ltbtwnnqq  7598  addnnnq0  7632  mulnnnq0  7633  prarloclemn  7682  prarloc  7686  distrlem1prl  7765  distrlem1pru  7766  distrlem4prl  7767  distrlem4pru  7768  ltexprlemrl  7793  cauappcvgprlemladdru  7839  cauappcvgprlemladdrl  7840  addsrpr  7928  mulsrpr  7929  map2psrprg  7988  axpre-suploclemres  8084  lemul12a  9005  lemulge11  9009  sup3exmid  9100  nngt0  9131  nn0ge0  9390  nn0ge2m1nn  9425  zletric  9486  zlelttric  9487  nn0n0n1ge2b  9522  nn0ind-raph  9560  supinfneg  9786  infsupneg  9787  infregelbex  9789  rpge0  9858  fz0fzelfz0  10319  fz0fzdiffz0  10322  ige2m2fzo  10399  elfzodifsumelfzo  10402  elfzom1elp1fzo  10403  exfzdc  10441  zsupcllemstep  10444  infssuzex  10448  qletric  10456  qlelttric  10457  rebtwn2zlemshrink  10468  frecuzrdgtcl  10629  frecuzrdg0  10630  frecuzrdgfunlem  10636  frecuzrdg0t  10639  frecuzrdgsuctlem  10640  frecfzennn  10643  seq3f1olemstep  10731  expcl2lemap  10768  leexp1a  10811  expnbnd  10880  faclbnd  10958  faclbnd6  10961  facavg  10963  fihasheqf1oi  11004  fihashf1rn  11005  fihashss  11033  fiubm  11045  seq3coll  11059  wrdsymb0  11099  wrdlenge2n0  11102  ccatsymb  11132  pfxnd  11216  pfxccat1  11229  swrdpfx  11234  pfxpfx  11235  wrd2ind  11250  pfxccatin12  11260  pfxccat3  11261  swrdccat  11262  pfxccatpfx1  11263  pfxccatpfx2  11264  swrdccatin1d  11270  pfxccatin12d  11272  resqrexlemdecn  11518  qabsor  11581  cau3lem  11620  xrmaxiflemab  11753  xrmaxadd  11767  climcn2  11815  sumeq2  11865  sumrbdclem  11883  summodclem3  11886  summodclem2a  11887  zsumdc  11890  fsumgcl  11892  fsum3  11893  isumss  11897  fsumadd  11912  fsum2dlemstep  11940  fisum0diag2  11953  fsummulc2  11954  modfsummodlemstep  11963  fsumabs  11971  fsumrelem  11977  fsumiun  11983  isumshft  11996  mertenslem2  12042  prodeq2  12063  prodrbdclem  12077  prodmodclem3  12081  prodmodclem2a  12082  zproddc  12085  fprodseq  12089  fprodmul  12097  fprodconst  12126  fprodap0  12127  fprod2dlemstep  12128  fprodrec  12135  fprodsplit1f  12140  fprodap0f  12142  fprodle  12146  sin02gt0  12270  efieq1re  12278  p1modz1  12300  dvdsleabs2  12352  4dvdseven  12423  bitsfzo  12461  bitsinv1lem  12467  gcdeq0  12493  rppwr  12544  uzwodc  12553  algfx  12569  eucalgcvga  12575  lcmmndc  12579  lcmeq0  12588  qredeq  12613  isprm3  12635  rpexp  12670  sqpweven  12692  2sqpwodd  12693  phicl2  12731  phibnd  12734  phiprmpw  12739  fermltl  12751  pythagtriplem4  12786  pythagtriplem6  12788  pythagtriplem7  12789  pythagtriplem12  12793  pythagtriplem13  12794  pythagtriplem14  12795  pythagtriplem16  12797  pcdvdsb  12838  pc2dvds  12848  difsqpwdvds  12856  pcmpt  12861  pcmptdvds  12863  fldivp1  12866  prmpwdvds  12873  infpnlem1  12877  1arith  12885  4sqlem11  12919  ennnfonelemk  12966  ennnfonelemhom  12981  ennnfonelemrnh  12982  ennnfonelemf1  12984  ctinf  12996  ctiunctlemudc  13003  ctiunctlemf  13004  nninfdclemp1  13016  strslfvd  13069  strslfv2d  13070  strslssd  13074  imasival  13334  imasbas  13335  imasplusg  13336  imasaddfnlemg  13342  imasaddvallemg  13343  qusaddvallemg  13361  qusaddflemg  13362  qusaddval  13363  qusaddf  13364  qusmulval  13365  qusmulf  13366  lidrididd  13410  gsumfzval  13419  sgrpidmndm  13448  gsumfzz  13523  qusgrp2  13645  mulgnegnn  13664  eqgen  13759  rinvmod  13841  gsumfzconst  13873  qusrng  13916  srgdilem  13927  ringdilem  13970  qusring2  14024  lssintclm  14342  gsumfzfsumlemm  14545  mplsubgfilemm  14656  eltg3  14725  iuncld  14783  cnss2  14895  txcnp  14939  uptx  14942  xblm  15085  metss  15162  fsumcncntop  15235  rescncf  15249  dedekindeulemlu  15289  suplociccex  15293  dedekindicclemlu  15298  dedekindicc  15301  ivthdec  15312  limccnp2lem  15344  dvaddxx  15371  dvmulxx  15372  dvrecap  15381  reeff1olem  15439  perfectlem2  15668  lgsval  15677  lgsfvalg  15678  lgsfcl2  15679  lgscllem  15680  lgsval2lem  15683  lgsneg  15697  lgsdir2  15706  lgsdir  15708  lgsdi  15710  lgsne0  15711  lgsdirnn0  15720  lgsdinn0  15721  gausslemma2dlem0c  15724  m1lgs  15758  2lgslem1  15764  2lgs  15777  2lgsoddprm  15786  2sqlem6  15793  incistruhgr  15884  upgredg  15936  uhgr2edg  15998  usgriedgdomord  16017  wlkpropg  16030  wlkvtxeledgg  16041  sumdc2  16121  pwle2  16323  subctctexmid  16325  nninfsellemeq  16339  nnnninfex  16347  exmidsbthrlem  16349  cndcap  16386