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  1310  xordidc  1410  nfimd  1596  exlimd2  1606  elex22  2775  elex2  2776  spcimdv  2845  spcimedv  2847  spcedv  2850  rspcdva  2870  elabd  2906  spsbcd  2999  opth  4267  euotd  4284  ssorduni  4520  tfisi  4620  omsinds  4655  nnpredcl  4656  sotri2  5064  sotri3  5065  unielrel  5194  funmo  5270  fnfvima  5794  fliftfun  5840  fliftval  5844  riota5f  5899  riotass2  5901  fovcld  6024  oprssdmm  6226  tfrlem5  6369  tfrlemibxssdm  6382  tfrlemibfn  6383  tfrlemiex  6386  tfr1onlemsucfn  6395  tfr1onlemsucaccv  6396  tfr1onlembxssdm  6398  tfr1onlembfn  6399  tfr1onlemex  6402  tfr1onlemres  6404  tfrcllemsucfn  6408  tfrcllemsucaccv  6409  tfrcllembxssdm  6411  tfrcllembfn  6412  tfrcllemex  6415  tfrcllemres  6417  tfrcl  6419  rdgisucinc  6440  frecabex  6453  frecabcl  6454  nntr2  6558  ertr  6604  qliftlem  6669  th3q  6696  resixp  6789  f1dom2g  6812  dom3d  6830  en1  6855  xpdom3m  6890  xpf1o  6902  phplem4dom  6920  phpm  6923  phpelm  6924  findcard  6946  finexdc  6960  fiintim  6987  fisseneq  6990  ssfirab  6992  opabfi  6994  f1dmvrnfibi  7005  iunfidisj  7007  fidcenumlemrk  7015  dcfi  7042  suplub2ti  7062  supelti  7063  ordiso2  7096  caseinl  7152  caseinr  7153  djudom  7154  difinfsn  7161  difinfinf  7162  ctm  7170  enumct  7176  nnnninfeq  7189  ismkvnex  7216  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  acfun  7269  exmidontriimlem2  7284  exmidontriimlem3  7285  exmidapne  7322  cc2lem  7328  cc3  7330  recexnq  7452  ltbtwnnqq  7477  addnnnq0  7511  mulnnnq0  7512  prarloclemn  7561  prarloc  7565  distrlem1prl  7644  distrlem1pru  7645  distrlem4prl  7646  distrlem4pru  7647  ltexprlemrl  7672  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  addsrpr  7807  mulsrpr  7808  map2psrprg  7867  axpre-suploclemres  7963  lemul12a  8883  lemulge11  8887  sup3exmid  8978  nngt0  9009  nn0ge0  9268  nn0ge2m1nn  9303  zletric  9364  zlelttric  9365  nn0n0n1ge2b  9399  nn0ind-raph  9437  supinfneg  9663  infsupneg  9664  infregelbex  9666  rpge0  9735  fz0fzelfz0  10196  fz0fzdiffz0  10199  ige2m2fzo  10268  elfzodifsumelfzo  10271  elfzom1elp1fzo  10272  exfzdc  10310  qletric  10314  qlelttric  10315  rebtwn2zlemshrink  10325  frecuzrdgtcl  10486  frecuzrdg0  10487  frecuzrdgfunlem  10493  frecuzrdg0t  10496  frecuzrdgsuctlem  10497  frecfzennn  10500  seq3f1olemstep  10588  expcl2lemap  10625  leexp1a  10668  expnbnd  10737  faclbnd  10815  faclbnd6  10818  facavg  10820  fihasheqf1oi  10861  fihashf1rn  10862  fihashss  10890  fiubm  10902  seq3coll  10916  wrdsymb0  10949  wrdlenge2n0  10952  resqrexlemdecn  11159  qabsor  11222  cau3lem  11261  xrmaxiflemab  11393  xrmaxadd  11407  climcn2  11455  sumeq2  11505  sumrbdclem  11523  summodclem3  11526  summodclem2a  11527  zsumdc  11530  fsumgcl  11532  fsum3  11533  isumss  11537  fsumadd  11552  fsum2dlemstep  11580  fisum0diag2  11593  fsummulc2  11594  modfsummodlemstep  11603  fsumabs  11611  fsumrelem  11617  fsumiun  11623  isumshft  11636  mertenslem2  11682  prodeq2  11703  prodrbdclem  11717  prodmodclem3  11721  prodmodclem2a  11722  zproddc  11725  fprodseq  11729  fprodmul  11737  fprodconst  11766  fprodap0  11767  fprod2dlemstep  11768  fprodrec  11775  fprodsplit1f  11780  fprodap0f  11782  fprodle  11786  sin02gt0  11910  efieq1re  11918  p1modz1  11940  dvdsleabs2  11991  4dvdseven  12061  zsupcllemstep  12085  infssuzex  12089  gcdeq0  12117  rppwr  12168  uzwodc  12177  algfx  12193  eucalgcvga  12199  lcmmndc  12203  lcmeq0  12212  qredeq  12237  isprm3  12259  rpexp  12294  sqpweven  12316  2sqpwodd  12317  phicl2  12355  phibnd  12358  phiprmpw  12363  fermltl  12375  pythagtriplem4  12409  pythagtriplem6  12411  pythagtriplem7  12412  pythagtriplem12  12416  pythagtriplem13  12417  pythagtriplem14  12418  pythagtriplem16  12420  pcdvdsb  12461  pc2dvds  12471  difsqpwdvds  12479  pcmpt  12484  pcmptdvds  12486  fldivp1  12489  prmpwdvds  12496  infpnlem1  12500  1arith  12508  4sqlem11  12542  ennnfonelemk  12560  ennnfonelemhom  12575  ennnfonelemrnh  12576  ennnfonelemf1  12578  ctinf  12590  ctiunctlemudc  12597  ctiunctlemf  12598  nninfdclemp1  12610  strslfvd  12663  strslfv2d  12664  strslssd  12668  imasival  12892  imasbas  12893  imasplusg  12894  imasaddfnlemg  12900  imasaddvallemg  12901  qusaddvallemg  12919  qusaddflemg  12920  qusaddval  12921  qusaddf  12922  qusmulval  12923  qusmulf  12924  lidrididd  12968  gsumfzval  12977  sgrpidmndm  13004  gsumfzz  13070  qusgrp2  13186  mulgnegnn  13205  eqgen  13300  rinvmod  13382  gsumfzconst  13414  qusrng  13457  srgdilem  13468  ringdilem  13511  qusring2  13565  lssintclm  13883  gsumfzfsumlemm  14086  eltg3  14236  iuncld  14294  cnss2  14406  txcnp  14450  uptx  14453  xblm  14596  metss  14673  fsumcncntop  14746  rescncf  14760  dedekindeulemlu  14800  suplociccex  14804  dedekindicclemlu  14809  dedekindicc  14812  ivthdec  14823  limccnp2lem  14855  dvaddxx  14882  dvmulxx  14883  dvrecap  14892  reeff1olem  14947  lgsval  15161  lgsfvalg  15162  lgsfcl2  15163  lgscllem  15164  lgsval2lem  15167  lgsneg  15181  lgsdir2  15190  lgsdir  15192  lgsdi  15194  lgsne0  15195  lgsdirnn0  15204  lgsdinn0  15205  gausslemma2dlem0c  15208  m1lgs  15242  2lgslem1  15248  2lgs  15261  2lgsoddprm  15270  2sqlem6  15277  sumdc2  15361  pwle2  15559  subctctexmid  15561  nninfsellemeq  15574  exmidsbthrlem  15582  cndcap  15619