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  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  3684  opth  4372  euotd  4390  ssorduni  4629  tfisi  4729  omsinds  4764  nnpredcl  4765  sotri2  5180  sotri3  5181  unielrel  5310  funmo  5387  fnfvima  5943  resfvresima  5946  fliftfun  5992  fliftval  5996  riota5f  6055  riotass2  6057  fovcld  6183  oprssdmm  6395  funsssuppss  6488  tfrlem5  6575  tfrlemibxssdm  6588  tfrlemibfn  6589  tfrlemiex  6592  tfr1onlemsucfn  6601  tfr1onlemsucaccv  6602  tfr1onlembxssdm  6604  tfr1onlembfn  6605  tfr1onlemex  6608  tfr1onlemres  6610  tfrcllemsucfn  6614  tfrcllemsucaccv  6615  tfrcllembxssdm  6617  tfrcllembfn  6618  tfrcllemex  6621  tfrcllemres  6623  tfrcl  6625  rdgisucinc  6646  frecabex  6659  frecabcl  6660  nntr2  6766  ertr  6812  qliftlem  6877  th3q  6904  resixp  7005  f1dom2g  7032  dom3d  7050  domssr  7054  en1  7076  xpdom3m  7122  xpf1o  7134  phplem4dom  7153  phpm  7157  phpelm  7158  findcard  7182  finexdc  7197  fiintim  7228  fisseneq  7232  ssfirab  7234  opabfi  7237  f1dmvrnfibi  7248  iunfidisj  7250  fidcenumlemrk  7261  dcfi  7305  fdcf1  7306  2omapfi  7310  suplub2ti  7331  supelti  7332  ordiso2  7365  caseinl  7421  caseinr  7422  djudom  7423  difinfsn  7430  difinfinf  7431  ctm  7439  enumct  7445  nnnninfeq  7458  ismkvnex  7485  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  acfun  7553  exmidontriimlem2  7568  exmidontriimlem3  7569  exmidapne  7616  cc2lem  7622  cc3  7624  recexnq  7747  ltbtwnnqq  7772  addnnnq0  7806  mulnnnq0  7807  prarloclemn  7856  prarloc  7860  distrlem1prl  7939  distrlem1pru  7940  distrlem4prl  7941  distrlem4pru  7942  ltexprlemrl  7967  cauappcvgprlemladdru  8013  cauappcvgprlemladdrl  8014  addsrpr  8102  mulsrpr  8103  map2psrprg  8162  axpre-suploclemres  8258  lemul12a  9182  lemulge11  9186  sup3exmid  9277  nngt0  9308  nn0ge0  9567  nn0ge2m1nn  9606  zletric  9667  zlelttric  9668  nn0n0n1ge2b  9704  nn0ind-raph  9742  supinfneg  9974  infsupneg  9975  infregelbex  9977  rpge0  10046  fz0fzelfz0  10512  fz0fzdiffz0  10515  ige2m2fzo  10594  elfzodifsumelfzo  10597  elfzom1elp1fzo  10598  exfzdc  10637  zsupcllemstep  10640  infssuzex  10644  qletric  10654  qlelttric  10655  rebtwn2zlemshrink  10666  frecuzrdgtcl  10827  frecuzrdg0  10828  frecuzrdgfunlem  10834  frecuzrdg0t  10837  frecuzrdgsuctlem  10838  frecfzennn  10841  seq3f1olemstep  10929  expcl2lemap  10966  leexp1a  11009  expnbnd  11079  faclbnd  11157  faclbnd6  11160  facavg  11162  fihasheqf1oi  11204  fihashf1rn  11205  fihashss  11235  fiubm  11249  seq3coll  11272  wrdsymb0  11315  wrdlenge2n0  11318  ccatsymb  11348  pfxnd  11439  pfxccat1  11452  swrdpfx  11457  pfxpfx  11458  wrd2ind  11473  pfxccatin12  11483  pfxccat3  11484  swrdccat  11485  pfxccatpfx1  11486  pfxccatpfx2  11487  swrdccatin1d  11493  pfxccatin12d  11495  resqrexlemdecn  11756  qabsor  11819  cau3lem  11858  xrmaxiflemab  11991  xrmaxadd  12005  climcn2  12053  sumeq2  12103  sumrbdclem  12122  summodclem3  12125  summodclem2a  12126  zsumdc  12129  fsumgcl  12131  fsum3  12132  isumss  12136  fsumadd  12151  fsum2dlemstep  12179  fisum0diag2  12192  fsummulc2  12193  modfsummodlemstep  12202  fsumabs  12210  fsumrelem  12216  fsumiun  12222  isumshft  12235  mertenslem2  12281  prodeq2  12302  prodrbdclem  12316  prodmodclem3  12320  prodmodclem2a  12321  zproddc  12324  fprodseq  12328  fprodmul  12336  fprodconst  12365  fprodap0  12366  fprod2dlemstep  12367  fprodrec  12374  fprodsplit1f  12379  fprodap0f  12381  fprodle  12385  sin02gt0  12509  efieq1re  12517  p1modz1  12539  dvdsleabs2  12591  4dvdseven  12662  bitsfzo  12700  bitsinv1lem  12706  gcdeq0  12732  rppwr  12783  uzwodc  12792  algfx  12808  eucalgcvga  12814  lcmmndc  12818  lcmeq0  12827  qredeq  12852  isprm3  12874  rpexp  12909  sqpweven  12931  2sqpwodd  12932  phicl2  12970  phibnd  12973  phiprmpw  12978  fermltl  12990  pythagtriplem4  13025  pythagtriplem6  13027  pythagtriplem7  13028  pythagtriplem12  13032  pythagtriplem13  13033  pythagtriplem14  13034  pythagtriplem16  13036  pcdvdsb  13077  pc2dvds  13087  difsqpwdvds  13095  pcmpt  13100  pcmptdvds  13102  fldivp1  13105  prmpwdvds  13112  infpnlem1  13116  1arith  13124  4sqlem11  13158  ballotfilemfp1  13209  ballotfilemic  13228  ennnfonelemk  13269  ennnfonelemhom  13284  ennnfonelemrnh  13285  ennnfonelemf1  13287  ctinf  13299  ctiunctlemudc  13306  ctiunctlemf  13307  nninfdclemp1  13319  strslfvd  13372  strslfv2d  13373  strslssd  13377  imasival  13604  imasbas  13605  imasplusg  13606  imasaddfnlemg  13612  imasaddvallemg  13613  qusaddvallemg  13631  qusaddflemg  13632  qusaddval  13633  qusaddf  13634  qusmulval  13635  qusmulf  13636  lidrididd  13679  gzsumfzval  13688  sgrpidmndm  13710  qusgrp2  13893  mulgnegnn  13912  eqgen  14007  rinvmod  14090  gzsumconst  14120  gsump1  14134  gsummptfidmadd  14138  qusrng  14232  srgdilem  14247  ringdilem  14290  qusring2  14344  lssintclm  14693  mplsubgfilemm  15012  eltg3  15081  iuncld  15139  cnss2  15251  txcnp  15295  uptx  15298  xblm  15441  metss  15518  fsumcncntop  15591  rescncf  15605  dedekindeulemlu  15645  suplociccex  15649  dedekindicclemlu  15654  dedekindicc  15657  ivthdec  15668  limccnp2lem  15700  dvaddxx  15727  dvmulxx  15728  dvrecap  15737  reeff1olem  15795  perfectlem2  16028  lgsval  16037  lgsfvalg  16038  lgsfcl2  16039  lgscllem  16040  lgsval2lem  16043  lgsneg  16057  lgsdir2  16066  lgsdir  16068  lgsdi  16070  lgsne0  16071  lgsdirnn0  16080  lgsdinn0  16081  gausslemma2dlem0c  16084  m1lgs  16118  2lgslem1  16124  2lgs  16137  2lgsoddprm  16146  2sqlem6  16153  incistruhgr  16245  upgredg  16299  uhgr2edg  16361  usgriedgdomord  16380  wlkpropg  16479  wlkvtxeledgg  16499  wlk2f  16506  clwwlknonccat  16588  clwwlknonex2lem2  16593  eupth2lem3lem4fi  16628  eupth2lem3lem7fi  16629  dichmul0orlem3  16669  sumdc2  16741  pwle2  16942  subctctexmid  16944  nninfsellemeq  16962  nnnninfex  16970  exmidsbthrlem  16972  cndcap  17014