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  1599  exlimd2  1609  elex22  2778  elex2  2779  spcimdv  2848  spcimedv  2850  spcedv  2853  rspcdva  2873  elabd  2909  spsbcd  3002  opth  4271  euotd  4288  ssorduni  4524  tfisi  4624  omsinds  4659  nnpredcl  4660  sotri2  5068  sotri3  5069  unielrel  5198  funmo  5274  fnfvima  5800  fliftfun  5846  fliftval  5850  riota5f  5905  riotass2  5907  fovcld  6031  oprssdmm  6238  tfrlem5  6381  tfrlemibxssdm  6394  tfrlemibfn  6395  tfrlemiex  6398  tfr1onlemsucfn  6407  tfr1onlemsucaccv  6408  tfr1onlembxssdm  6410  tfr1onlembfn  6411  tfr1onlemex  6414  tfr1onlemres  6416  tfrcllemsucfn  6420  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllembfn  6424  tfrcllemex  6427  tfrcllemres  6429  tfrcl  6431  rdgisucinc  6452  frecabex  6465  frecabcl  6466  nntr2  6570  ertr  6616  qliftlem  6681  th3q  6708  resixp  6801  f1dom2g  6824  dom3d  6842  en1  6867  xpdom3m  6902  xpf1o  6914  phplem4dom  6932  phpm  6935  phpelm  6936  findcard  6958  finexdc  6972  fiintim  7001  fisseneq  7004  ssfirab  7006  opabfi  7008  f1dmvrnfibi  7019  iunfidisj  7021  fidcenumlemrk  7029  dcfi  7056  suplub2ti  7076  supelti  7077  ordiso2  7110  caseinl  7166  caseinr  7167  djudom  7168  difinfsn  7175  difinfinf  7176  ctm  7184  enumct  7190  nnnninfeq  7203  ismkvnex  7230  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  acfun  7290  exmidontriimlem2  7305  exmidontriimlem3  7306  exmidapne  7343  cc2lem  7349  cc3  7351  recexnq  7474  ltbtwnnqq  7499  addnnnq0  7533  mulnnnq0  7534  prarloclemn  7583  prarloc  7587  distrlem1prl  7666  distrlem1pru  7667  distrlem4prl  7668  distrlem4pru  7669  ltexprlemrl  7694  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  addsrpr  7829  mulsrpr  7830  map2psrprg  7889  axpre-suploclemres  7985  lemul12a  8906  lemulge11  8910  sup3exmid  9001  nngt0  9032  nn0ge0  9291  nn0ge2m1nn  9326  zletric  9387  zlelttric  9388  nn0n0n1ge2b  9422  nn0ind-raph  9460  supinfneg  9686  infsupneg  9687  infregelbex  9689  rpge0  9758  fz0fzelfz0  10219  fz0fzdiffz0  10222  ige2m2fzo  10291  elfzodifsumelfzo  10294  elfzom1elp1fzo  10295  exfzdc  10333  zsupcllemstep  10336  infssuzex  10340  qletric  10348  qlelttric  10349  rebtwn2zlemshrink  10360  frecuzrdgtcl  10521  frecuzrdg0  10522  frecuzrdgfunlem  10528  frecuzrdg0t  10531  frecuzrdgsuctlem  10532  frecfzennn  10535  seq3f1olemstep  10623  expcl2lemap  10660  leexp1a  10703  expnbnd  10772  faclbnd  10850  faclbnd6  10853  facavg  10855  fihasheqf1oi  10896  fihashf1rn  10897  fihashss  10925  fiubm  10937  seq3coll  10951  wrdsymb0  10984  wrdlenge2n0  10987  resqrexlemdecn  11194  qabsor  11257  cau3lem  11296  xrmaxiflemab  11429  xrmaxadd  11443  climcn2  11491  sumeq2  11541  sumrbdclem  11559  summodclem3  11562  summodclem2a  11563  zsumdc  11566  fsumgcl  11568  fsum3  11569  isumss  11573  fsumadd  11588  fsum2dlemstep  11616  fisum0diag2  11629  fsummulc2  11630  modfsummodlemstep  11639  fsumabs  11647  fsumrelem  11653  fsumiun  11659  isumshft  11672  mertenslem2  11718  prodeq2  11739  prodrbdclem  11753  prodmodclem3  11757  prodmodclem2a  11758  zproddc  11761  fprodseq  11765  fprodmul  11773  fprodconst  11802  fprodap0  11803  fprod2dlemstep  11804  fprodrec  11811  fprodsplit1f  11816  fprodap0f  11818  fprodle  11822  sin02gt0  11946  efieq1re  11954  p1modz1  11976  dvdsleabs2  12028  4dvdseven  12099  bitsfzo  12137  bitsinv1lem  12143  gcdeq0  12169  rppwr  12220  uzwodc  12229  algfx  12245  eucalgcvga  12251  lcmmndc  12255  lcmeq0  12264  qredeq  12289  isprm3  12311  rpexp  12346  sqpweven  12368  2sqpwodd  12369  phicl2  12407  phibnd  12410  phiprmpw  12415  fermltl  12427  pythagtriplem4  12462  pythagtriplem6  12464  pythagtriplem7  12465  pythagtriplem12  12469  pythagtriplem13  12470  pythagtriplem14  12471  pythagtriplem16  12473  pcdvdsb  12514  pc2dvds  12524  difsqpwdvds  12532  pcmpt  12537  pcmptdvds  12539  fldivp1  12542  prmpwdvds  12549  infpnlem1  12553  1arith  12561  4sqlem11  12595  ennnfonelemk  12642  ennnfonelemhom  12657  ennnfonelemrnh  12658  ennnfonelemf1  12660  ctinf  12672  ctiunctlemudc  12679  ctiunctlemf  12680  nninfdclemp1  12692  strslfvd  12745  strslfv2d  12746  strslssd  12750  imasival  13008  imasbas  13009  imasplusg  13010  imasaddfnlemg  13016  imasaddvallemg  13017  qusaddvallemg  13035  qusaddflemg  13036  qusaddval  13037  qusaddf  13038  qusmulval  13039  qusmulf  13040  lidrididd  13084  gsumfzval  13093  sgrpidmndm  13122  gsumfzz  13197  qusgrp2  13319  mulgnegnn  13338  eqgen  13433  rinvmod  13515  gsumfzconst  13547  qusrng  13590  srgdilem  13601  ringdilem  13644  qusring2  13698  lssintclm  14016  gsumfzfsumlemm  14219  eltg3  14377  iuncld  14435  cnss2  14547  txcnp  14591  uptx  14594  xblm  14737  metss  14814  fsumcncntop  14887  rescncf  14901  dedekindeulemlu  14941  suplociccex  14945  dedekindicclemlu  14950  dedekindicc  14953  ivthdec  14964  limccnp2lem  14996  dvaddxx  15023  dvmulxx  15024  dvrecap  15033  reeff1olem  15091  perfectlem2  15320  lgsval  15329  lgsfvalg  15330  lgsfcl2  15331  lgscllem  15332  lgsval2lem  15335  lgsneg  15349  lgsdir2  15358  lgsdir  15360  lgsdi  15362  lgsne0  15363  lgsdirnn0  15372  lgsdinn0  15373  gausslemma2dlem0c  15376  m1lgs  15410  2lgslem1  15416  2lgs  15429  2lgsoddprm  15438  2sqlem6  15445  sumdc2  15529  pwle2  15729  subctctexmid  15731  nninfsellemeq  15745  exmidsbthrlem  15753  cndcap  15790