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 ⊢ (𝜑 → 𝜃)

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  4379  euotd  4397  ssorduni  4636  tfisi  4736  omsinds  4771  nnpredcl  4772  sotri2  5188  sotri3  5189  unielrel  5318  funmo  5395  fnfvima  5956  resfvresima  5959  fliftfun  6005  fliftval  6009  riota5f  6068  riotass2  6070  fovcld  6196  oprssdmm  6409  funsssuppss  6502  tfrlem5  6589  tfrlemibxssdm  6602  tfrlemibfn  6603  tfrlemiex  6606  tfr1onlemsucfn  6615  tfr1onlemsucaccv  6616  tfr1onlembxssdm  6618  tfr1onlembfn  6619  tfr1onlemex  6622  tfr1onlemres  6624  tfrcllemsucfn  6628  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllembfn  6632  tfrcllemex  6635  tfrcllemres  6637  tfrcl  6639  rdgisucinc  6660  frecabex  6673  frecabcl  6674  nntr2  6780  ertr  6826  qliftlem  6891  th3q  6918  resixp  7019  f1dom2g  7046  dom3d  7064  domssr  7068  en1  7090  xpdom3m  7136  xpf1o  7148  phplem4dom  7167  phpm  7171  phpelm  7172  findcard  7196  finexdc  7211  fiintim  7242  fisseneq  7246  ssfirab  7248  opabfi  7251  f1dmvrnfibi  7262  iunfidisj  7264  fidcenumlemrk  7276  dcfi  7320  fdcf1  7321  2omapfi  7326  suplub2ti  7347  supelti  7348  ordiso2  7381  caseinl  7437  caseinr  7438  djudom  7439  difinfsn  7446  difinfinf  7447  ctm  7455  enumct  7461  nnnninfeq  7474  ismkvnex  7501  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  acfun  7569  exmidontriimlem2  7584  exmidontriimlem3  7585  exmidapne  7632  cc2lem  7638  cc3  7640  recexnq  7763  ltbtwnnqq  7788  addnnnq0  7822  mulnnnq0  7823  prarloclemn  7872  prarloc  7876  distrlem1prl  7955  distrlem1pru  7956  distrlem4prl  7957  distrlem4pru  7958  ltexprlemrl  7983  cauappcvgprlemladdru  8029  cauappcvgprlemladdrl  8030  addsrpr  8118  mulsrpr  8119  map2psrprg  8178  axpre-suploclemres  8274  lemul12a  9200  lemulge11  9204  sup3exmid  9295  nngt0  9338  nn0ge0  9599  nn0ge2m1nn  9638  zletric  9699  zlelttric  9700  nn0n0n1ge2b  9736  nn0ind-raph  9774  supinfneg  10011  infsupneg  10012  infregelbex  10014  rpge0  10084  fz0fzelfz0  10551  fz0fzdiffz0  10554  ige2m2fzo  10633  elfzodifsumelfzo  10636  elfzom1elp1fzo  10637  exfzdc  10676  zsupcllemstep  10679  infssuzex  10683  qletric  10693  qlelttric  10694  rebtwn2zlemshrink  10705  frecuzrdgtcl  10870  frecuzrdg0  10871  frecuzrdgfunlem  10877  frecuzrdg0t  10880  frecuzrdgsuctlem  10881  frecfzennn  10884  seq3f1olemstep  10972  expcl2lemap  11009  leexp1a  11052  expnbnd  11122  faclbnd  11201  faclbnd6  11204  facavg  11206  fihasheqf1oi  11248  fihashf1rn  11249  fihashss  11279  fiubm  11293  seq3coll  11316  wrdsymb0  11359  wrdlenge2n0  11362  ccatsymb  11392  pfxnd  11483  pfxccat1  11496  swrdpfx  11501  pfxpfx  11502  wrd2ind  11517  pfxccatin12  11527  pfxccat3  11528  swrdccat  11529  pfxccatpfx1  11530  pfxccatpfx2  11531  swrdccatin1d  11537  pfxccatin12d  11539  resqrexlemdecn  11800  qabsor  11863  cau3lem  11903  xrmaxiflemab  12038  xrmaxadd  12052  climcn2  12100  sumeq2  12150  sumrbdclem  12169  summodclem3  12172  summodclem2a  12173  zsumdc  12176  fsumgcl  12178  fsum3  12179  isumss  12183  fsumadd  12198  fsum2dlemstep  12226  fisum0diag2  12239  fsummulc2  12240  modfsummodlemstep  12249  fsumabs  12257  fsumrelem  12263  fsumiun  12269  isumshft  12282  mertenslem2  12328  prodeq2  12349  prodrbdclem  12363  prodmodclem3  12367  prodmodclem2a  12368  zproddc  12371  fprodseq  12375  fprodmul  12383  fprodconst  12412  fprodap0  12413  fprod2dlemstep  12414  fprodrec  12421  fprodsplit1f  12426  fprodap0f  12428  fprodle  12432  sin02gt0  12556  efieq1re  12564  p1modz1  12586  dvdsleabs2  12638  4dvdseven  12709  bitsfzo  12747  bitsinv1lem  12753  gcdeq0  12779  rppwr  12830  uzwodc  12839  algfx  12855  eucalgcvga  12861  lcmmndc  12865  lcmeq0  12874  qredeq  12899  isprm3  12921  rpexp  12957  sqpweven  12980  2sqpwodd  12981  phicl2  13021  phibnd  13024  phiprmpw  13029  fermltl  13041  pythagtriplem4  13076  pythagtriplem6  13078  pythagtriplem7  13079  pythagtriplem12  13083  pythagtriplem13  13084  pythagtriplem14  13085  pythagtriplem16  13087  pcdvdsb  13128  pc2dvds  13138  difsqpwdvds  13146  pcmpt  13151  pcmptdvds  13153  fldivp1  13156  prmpwdvds  13163  infpnlem1  13167  1arith  13175  4sqlem11  13209  prmlem1  13251  prmlem2  13263  ballotfilemfp1  13289  ballotfilemic  13308  ennnfonelemk  13349  ennnfonelemhom  13364  ennnfonelemrnh  13365  ennnfonelemf1  13367  ctinf  13379  ctiunctlemudc  13386  ctiunctlemf  13387  nninfdclemp1  13399  strslfvd  13452  strslfv2d  13453  strslssd  13457  imasival  13686  imasbas  13687  imasplusg  13688  imasaddfnlemg  13694  imasaddvallemg  13695  qusaddvallemg  13713  qusaddflemg  13714  qusaddval  13715  qusaddf  13716  qusmulval  13717  qusmulf  13718  lidrididd  13761  gzsumfzval  13770  sgrpidmndm  13792  qusgrp2  13975  mulgnegnn  13994  eqgen  14089  rinvmod  14203  gzsumconst  14233  gsump1  14247  gsummptfidmadd  14251  gsummptfidmsplit  14254  gsumresfi  14263  qusrng  14364  srgdilem  14380  ringdilem  14423  qusring2  14480  lssintclm  14830  mplsubgfilemm  15214  eltg3  15283  iuncld  15341  cnss2  15453  txcnp  15497  uptx  15500  xblm  15643  metss  15720  fsumcncntop  15793  rescncf  15807  dedekindeulemlu  15847  suplociccex  15851  dedekindicclemlu  15856  dedekindicc  15859  ivthdec  15870  limccnp2lem  15902  dvaddxx  15929  dvmulxx  15930  dvrecap  15939  reeff1olem  15997  ppiqwordi  16268  ppiqeq0  16280  ppiqub  16293  perfectlem2  16300  lgsval  16328  lgsfvalg  16329  lgsfcl2  16330  lgscllem  16331  lgsval2lem  16334  lgsneg  16348  lgsdir2  16357  lgsdir  16359  lgsdi  16361  lgsne0  16362  lgsdirnn0  16371  lgsdinn0  16372  gausslemma2dlem0c  16375  m1lgs  16409  2lgslem1  16415  2lgs  16428  2lgsoddprm  16437  2sqlem6  16444  incistruhgr  16536  upgredg  16590  uhgr2edg  16652  usgriedgdomord  16671  wlkpropg  16770  wlkvtxeledgg  16790  wlk2f  16797  clwwlknonccat  16879  clwwlknonex2lem2  16884  eupth2lem3lem4fi  16919  eupth2lem3lem7fi  16920  dichmul0orlem3  16960  sumdc2  17032  pwle2  17233  subctctexmid  17235  nninfsellemeq  17263  nnnninfex  17271  exmidsbthrlem  17273  cndcap  17316