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  123  2thd  174  jca  304  syl2anc  409  jc  640  jcnd  642  annimdc  926  orandc  928  dn1dc  949  syl2an23an  1288  xordidc  1388  nfimd  1572  exlimd2  1582  elex22  2736  elex2  2737  spcimdv  2805  spcimedv  2807  spcedv  2810  rspcdva  2830  elabd  2866  spsbcd  2958  opth  4209  euotd  4226  ssorduni  4458  tfisi  4558  omsinds  4593  nnpredcl  4594  sotri2  4995  sotri3  4996  unielrel  5125  funmo  5197  fnfvima  5713  fliftfun  5758  fliftval  5762  riota5f  5816  riotass2  5818  oprssdmm  6131  tfrlem5  6273  tfrlemibxssdm  6286  tfrlemibfn  6287  tfrlemiex  6290  tfr1onlemsucfn  6299  tfr1onlemsucaccv  6300  tfr1onlembxssdm  6302  tfr1onlembfn  6303  tfr1onlemex  6306  tfr1onlemres  6308  tfrcllemsucfn  6312  tfrcllemsucaccv  6313  tfrcllembxssdm  6315  tfrcllembfn  6316  tfrcllemex  6319  tfrcllemres  6321  tfrcl  6323  rdgisucinc  6344  frecabex  6357  frecabcl  6358  nntr2  6462  ertr  6507  qliftlem  6570  th3q  6597  resixp  6690  f1dom2g  6713  dom3d  6731  en1  6756  xpdom3m  6791  xpf1o  6801  phplem4dom  6819  phpm  6822  phpelm  6823  findcard  6845  finexdc  6859  fiintim  6885  fisseneq  6888  ssfirab  6890  f1dmvrnfibi  6900  iunfidisj  6902  fidcenumlemrk  6910  dcfi  6937  suplub2ti  6957  supelti  6958  ordiso2  6991  caseinl  7047  caseinr  7048  djudom  7049  difinfsn  7056  difinfinf  7057  ctm  7065  enumct  7071  nnnninfeq  7083  ismkvnex  7110  exmidfodomrlemr  7149  exmidfodomrlemrALT  7150  acfun  7154  exmidontriimlem2  7169  exmidontriimlem3  7170  cc2lem  7198  cc3  7200  recexnq  7322  ltbtwnnqq  7347  addnnnq0  7381  mulnnnq0  7382  prarloclemn  7431  prarloc  7435  distrlem1prl  7514  distrlem1pru  7515  distrlem4prl  7516  distrlem4pru  7517  ltexprlemrl  7542  cauappcvgprlemladdru  7588  cauappcvgprlemladdrl  7589  addsrpr  7677  mulsrpr  7678  map2psrprg  7737  axpre-suploclemres  7833  lemul12a  8748  lemulge11  8752  sup3exmid  8843  nngt0  8873  nn0ge0  9130  nn0ge2m1nn  9165  zletric  9226  zlelttric  9227  nn0n0n1ge2b  9261  nn0ind-raph  9299  supinfneg  9524  infsupneg  9525  infregelbex  9527  rpge0  9593  fz0fzelfz0  10052  fz0fzdiffz0  10055  ige2m2fzo  10123  elfzodifsumelfzo  10126  elfzom1elp1fzo  10127  exfzdc  10165  qletric  10169  qlelttric  10170  rebtwn2zlemshrink  10179  frecuzrdgtcl  10337  frecuzrdg0  10338  frecuzrdgfunlem  10344  frecuzrdg0t  10347  frecuzrdgsuctlem  10348  frecfzennn  10351  seq3f1olemstep  10426  expcl2lemap  10457  leexp1a  10500  expnbnd  10567  faclbnd  10643  faclbnd6  10646  facavg  10648  fihasheqf1oi  10690  fihashf1rn  10691  fihashss  10718  seq3coll  10741  resqrexlemdecn  10940  qabsor  11003  cau3lem  11042  xrmaxiflemab  11174  xrmaxadd  11188  climcn2  11236  sumeq2  11286  sumrbdclem  11304  summodclem3  11307  summodclem2a  11308  zsumdc  11311  fsumgcl  11313  fsum3  11314  isumss  11318  fsumadd  11333  fsum2dlemstep  11361  fisum0diag2  11374  fsummulc2  11375  modfsummodlemstep  11384  fsumabs  11392  fsumrelem  11398  fsumiun  11404  isumshft  11417  mertenslem2  11463  prodeq2  11484  prodrbdclem  11498  prodmodclem3  11502  prodmodclem2a  11503  zproddc  11506  fprodseq  11510  fprodmul  11518  fprodconst  11547  fprodap0  11548  fprod2dlemstep  11549  fprodrec  11556  fprodsplit1f  11561  fprodap0f  11563  fprodle  11567  sin02gt0  11690  efieq1re  11698  p1modz1  11720  dvdsleabs2  11769  4dvdseven  11839  gcdmndc  11862  zsupcllemstep  11863  infssuzex  11867  gcdsupex  11875  gcdsupcl  11876  gcdeq0  11895  gcdaddm  11902  rppwr  11946  algfx  11963  eucalgcvga  11969  lcmmndc  11973  lcmval  11974  lcmcllem  11978  lcmledvds  11981  lcmeq0  11982  qredeq  12007  isprm3  12029  prmdc  12041  rpexp  12062  sqpweven  12084  2sqpwodd  12085  phicl2  12123  phibnd  12126  phiprmpw  12131  fermltl  12143  pythagtriplem4  12177  pythagtriplem6  12179  pythagtriplem7  12180  pythagtriplem12  12184  pythagtriplem13  12185  pythagtriplem14  12186  pythagtriplem16  12188  pclemdc  12197  pcdvdsb  12228  pc2dvds  12238  difsqpwdvds  12246  pcmpt  12250  pcmptdvds  12252  fldivp1  12255  ennnfonelemk  12270  ennnfonelemhom  12285  ennnfonelemrnh  12286  ennnfonelemf1  12288  ctinf  12300  ctiunctlemudc  12307  ctiunctlemf  12308  nninfdclemcl  12320  nninfdclemp1  12322  strslfvd  12372  strslfv2d  12373  strslssd  12377  eltg3  12598  iuncld  12656  cnss2  12768  txcnp  12812  uptx  12815  xblm  12958  metss  13035  fsumcncntop  13097  rescncf  13109  dedekindeulemlu  13140  suplociccex  13144  dedekindicclemlu  13149  dedekindicc  13152  ivthdec  13163  limccnp2lem  13186  dvaddxx  13208  dvmulxx  13209  dvrecap  13218  reeff1olem  13233  sumdc2  13515  pwle2  13712  subctctexmid  13715  nninfsellemeq  13728  exmidsbthrlem  13735