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  650  jcnd  652  annimdc  937  orandc  939  dn1dc  960  syl2an23an  1299  xordidc  1399  nfimd  1583  exlimd2  1593  elex22  2750  elex2  2751  spcimdv  2819  spcimedv  2821  spcedv  2824  rspcdva  2844  elabd  2880  spsbcd  2973  opth  4231  euotd  4248  ssorduni  4480  tfisi  4580  omsinds  4615  nnpredcl  4616  sotri2  5018  sotri3  5019  unielrel  5148  funmo  5223  fnfvima  5742  fliftfun  5787  fliftval  5791  riota5f  5845  riotass2  5847  oprssdmm  6162  tfrlem5  6305  tfrlemibxssdm  6318  tfrlemibfn  6319  tfrlemiex  6322  tfr1onlemsucfn  6331  tfr1onlemsucaccv  6332  tfr1onlembxssdm  6334  tfr1onlembfn  6335  tfr1onlemex  6338  tfr1onlemres  6340  tfrcllemsucfn  6344  tfrcllemsucaccv  6345  tfrcllembxssdm  6347  tfrcllembfn  6348  tfrcllemex  6351  tfrcllemres  6353  tfrcl  6355  rdgisucinc  6376  frecabex  6389  frecabcl  6390  nntr2  6494  ertr  6540  qliftlem  6603  th3q  6630  resixp  6723  f1dom2g  6746  dom3d  6764  en1  6789  xpdom3m  6824  xpf1o  6834  phplem4dom  6852  phpm  6855  phpelm  6856  findcard  6878  finexdc  6892  fiintim  6918  fisseneq  6921  ssfirab  6923  f1dmvrnfibi  6933  iunfidisj  6935  fidcenumlemrk  6943  dcfi  6970  suplub2ti  6990  supelti  6991  ordiso2  7024  caseinl  7080  caseinr  7081  djudom  7082  difinfsn  7089  difinfinf  7090  ctm  7098  enumct  7104  nnnninfeq  7116  ismkvnex  7143  exmidfodomrlemr  7191  exmidfodomrlemrALT  7192  acfun  7196  exmidontriimlem2  7211  exmidontriimlem3  7212  cc2lem  7240  cc3  7242  recexnq  7364  ltbtwnnqq  7389  addnnnq0  7423  mulnnnq0  7424  prarloclemn  7473  prarloc  7477  distrlem1prl  7556  distrlem1pru  7557  distrlem4prl  7558  distrlem4pru  7559  ltexprlemrl  7584  cauappcvgprlemladdru  7630  cauappcvgprlemladdrl  7631  addsrpr  7719  mulsrpr  7720  map2psrprg  7779  axpre-suploclemres  7875  lemul12a  8790  lemulge11  8794  sup3exmid  8885  nngt0  8915  nn0ge0  9172  nn0ge2m1nn  9207  zletric  9268  zlelttric  9269  nn0n0n1ge2b  9303  nn0ind-raph  9341  supinfneg  9566  infsupneg  9567  infregelbex  9569  rpge0  9635  fz0fzelfz0  10095  fz0fzdiffz0  10098  ige2m2fzo  10166  elfzodifsumelfzo  10169  elfzom1elp1fzo  10170  exfzdc  10208  qletric  10212  qlelttric  10213  rebtwn2zlemshrink  10222  frecuzrdgtcl  10380  frecuzrdg0  10381  frecuzrdgfunlem  10387  frecuzrdg0t  10390  frecuzrdgsuctlem  10391  frecfzennn  10394  seq3f1olemstep  10469  expcl2lemap  10500  leexp1a  10543  expnbnd  10611  faclbnd  10687  faclbnd6  10690  facavg  10692  fihasheqf1oi  10733  fihashf1rn  10734  fihashss  10762  fiubm  10774  seq3coll  10788  resqrexlemdecn  10987  qabsor  11050  cau3lem  11089  xrmaxiflemab  11221  xrmaxadd  11235  climcn2  11283  sumeq2  11333  sumrbdclem  11351  summodclem3  11354  summodclem2a  11355  zsumdc  11358  fsumgcl  11360  fsum3  11361  isumss  11365  fsumadd  11380  fsum2dlemstep  11408  fisum0diag2  11421  fsummulc2  11422  modfsummodlemstep  11431  fsumabs  11439  fsumrelem  11445  fsumiun  11451  isumshft  11464  mertenslem2  11510  prodeq2  11531  prodrbdclem  11545  prodmodclem3  11549  prodmodclem2a  11550  zproddc  11553  fprodseq  11557  fprodmul  11565  fprodconst  11594  fprodap0  11595  fprod2dlemstep  11596  fprodrec  11603  fprodsplit1f  11608  fprodap0f  11610  fprodle  11614  sin02gt0  11737  efieq1re  11745  p1modz1  11767  dvdsleabs2  11817  4dvdseven  11887  gcdmndc  11910  zsupcllemstep  11911  infssuzex  11915  gcdsupex  11923  gcdsupcl  11924  gcdeq0  11943  gcdaddm  11950  rppwr  11994  uzwodc  12003  nnwosdc  12005  algfx  12017  eucalgcvga  12023  lcmmndc  12027  lcmval  12028  lcmcllem  12032  lcmledvds  12035  lcmeq0  12036  qredeq  12061  isprm3  12083  prmdc  12095  rpexp  12118  sqpweven  12140  2sqpwodd  12141  phicl2  12179  phibnd  12182  phiprmpw  12187  fermltl  12199  pythagtriplem4  12233  pythagtriplem6  12235  pythagtriplem7  12236  pythagtriplem12  12240  pythagtriplem13  12241  pythagtriplem14  12242  pythagtriplem16  12244  pclemdc  12253  pcdvdsb  12284  pc2dvds  12294  difsqpwdvds  12302  pcmpt  12306  pcmptdvds  12308  fldivp1  12311  prmpwdvds  12318  infpnlem1  12322  infpnlem2  12323  1arith  12330  ennnfonelemk  12366  ennnfonelemhom  12381  ennnfonelemrnh  12382  ennnfonelemf1  12384  ctinf  12396  ctiunctlemudc  12403  ctiunctlemf  12404  nninfdclemcl  12414  nninfdclemp1  12416  strslfvd  12468  strslfv2d  12469  strslssd  12473  lidrididd  12665  sgrpidmndm  12685  mulgnegnn  12852  rinvmod  12908  srgdilem  12945  ringdilem  12988  eltg3  13108  iuncld  13166  cnss2  13278  txcnp  13322  uptx  13325  xblm  13468  metss  13545  fsumcncntop  13607  rescncf  13619  dedekindeulemlu  13650  suplociccex  13654  dedekindicclemlu  13659  dedekindicc  13662  ivthdec  13673  limccnp2lem  13696  dvaddxx  13718  dvmulxx  13719  dvrecap  13728  reeff1olem  13743  lgsval  13956  lgsfvalg  13957  lgsfcl2  13958  lgscllem  13959  lgsval2lem  13962  lgsneg  13976  lgsdir2  13985  lgsdir  13987  lgsdi  13989  lgsne0  13990  lgsdirnn0  13999  lgsdinn0  14000  2sqlem6  14007  sumdc2  14091  pwle2  14288  subctctexmid  14291  nninfsellemeq  14304  exmidsbthrlem  14311