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  4377  euotd  4395  ssorduni  4634  tfisi  4734  omsinds  4769  nnpredcl  4770  sotri2  5185  sotri3  5186  unielrel  5315  funmo  5392  fnfvima  5953  resfvresima  5956  fliftfun  6002  fliftval  6006  riota5f  6065  riotass2  6067  fovcld  6193  oprssdmm  6405  funsssuppss  6498  tfrlem5  6585  tfrlemibxssdm  6598  tfrlemibfn  6599  tfrlemiex  6602  tfr1onlemsucfn  6611  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemex  6618  tfr1onlemres  6620  tfrcllemsucfn  6624  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemex  6631  tfrcllemres  6633  tfrcl  6635  rdgisucinc  6656  frecabex  6669  frecabcl  6670  nntr2  6776  ertr  6822  qliftlem  6887  th3q  6914  resixp  7015  f1dom2g  7042  dom3d  7060  domssr  7064  en1  7086  xpdom3m  7132  xpf1o  7144  phplem4dom  7163  phpm  7167  phpelm  7168  findcard  7192  finexdc  7207  fiintim  7238  fisseneq  7242  ssfirab  7244  opabfi  7247  f1dmvrnfibi  7258  iunfidisj  7260  fidcenumlemrk  7271  dcfi  7315  fdcf1  7316  2omapfi  7320  suplub2ti  7341  supelti  7342  ordiso2  7375  caseinl  7431  caseinr  7432  djudom  7433  difinfsn  7440  difinfinf  7441  ctm  7449  enumct  7455  nnnninfeq  7468  ismkvnex  7495  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  acfun  7563  exmidontriimlem2  7578  exmidontriimlem3  7579  exmidapne  7626  cc2lem  7632  cc3  7634  recexnq  7757  ltbtwnnqq  7782  addnnnq0  7816  mulnnnq0  7817  prarloclemn  7866  prarloc  7870  distrlem1prl  7949  distrlem1pru  7950  distrlem4prl  7951  distrlem4pru  7952  ltexprlemrl  7977  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  addsrpr  8112  mulsrpr  8113  map2psrprg  8172  axpre-suploclemres  8268  lemul12a  9194  lemulge11  9198  sup3exmid  9289  nngt0  9331  nn0ge0  9592  nn0ge2m1nn  9631  zletric  9692  zlelttric  9693  nn0n0n1ge2b  9729  nn0ind-raph  9767  supinfneg  10004  infsupneg  10005  infregelbex  10007  rpge0  10077  fz0fzelfz0  10544  fz0fzdiffz0  10547  ige2m2fzo  10626  elfzodifsumelfzo  10629  elfzom1elp1fzo  10630  exfzdc  10669  zsupcllemstep  10672  infssuzex  10676  qletric  10686  qlelttric  10687  rebtwn2zlemshrink  10698  frecuzrdgtcl  10862  frecuzrdg0  10863  frecuzrdgfunlem  10869  frecuzrdg0t  10872  frecuzrdgsuctlem  10873  frecfzennn  10876  seq3f1olemstep  10964  expcl2lemap  11001  leexp1a  11044  expnbnd  11114  faclbnd  11193  faclbnd6  11196  facavg  11198  fihasheqf1oi  11240  fihashf1rn  11241  fihashss  11271  fiubm  11285  seq3coll  11308  wrdsymb0  11351  wrdlenge2n0  11354  ccatsymb  11384  pfxnd  11475  pfxccat1  11488  swrdpfx  11493  pfxpfx  11494  wrd2ind  11509  pfxccatin12  11519  pfxccat3  11520  swrdccat  11521  pfxccatpfx1  11522  pfxccatpfx2  11523  swrdccatin1d  11529  pfxccatin12d  11531  resqrexlemdecn  11792  qabsor  11855  cau3lem  11895  xrmaxiflemab  12029  xrmaxadd  12043  climcn2  12091  sumeq2  12141  sumrbdclem  12160  summodclem3  12163  summodclem2a  12164  zsumdc  12167  fsumgcl  12169  fsum3  12170  isumss  12174  fsumadd  12189  fsum2dlemstep  12217  fisum0diag2  12230  fsummulc2  12231  modfsummodlemstep  12240  fsumabs  12248  fsumrelem  12254  fsumiun  12260  isumshft  12273  mertenslem2  12319  prodeq2  12340  prodrbdclem  12354  prodmodclem3  12358  prodmodclem2a  12359  zproddc  12362  fprodseq  12366  fprodmul  12374  fprodconst  12403  fprodap0  12404  fprod2dlemstep  12405  fprodrec  12412  fprodsplit1f  12417  fprodap0f  12419  fprodle  12423  sin02gt0  12547  efieq1re  12555  p1modz1  12577  dvdsleabs2  12629  4dvdseven  12700  bitsfzo  12738  bitsinv1lem  12744  gcdeq0  12770  rppwr  12821  uzwodc  12830  algfx  12846  eucalgcvga  12852  lcmmndc  12856  lcmeq0  12865  qredeq  12890  isprm3  12912  rpexp  12948  sqpweven  12971  2sqpwodd  12972  phicl2  13012  phibnd  13015  phiprmpw  13020  fermltl  13032  pythagtriplem4  13067  pythagtriplem6  13069  pythagtriplem7  13070  pythagtriplem12  13074  pythagtriplem13  13075  pythagtriplem14  13076  pythagtriplem16  13078  pcdvdsb  13119  pc2dvds  13129  difsqpwdvds  13137  pcmpt  13142  pcmptdvds  13144  fldivp1  13147  prmpwdvds  13154  infpnlem1  13158  1arith  13166  4sqlem11  13200  prmlem1  13242  prmlem2  13254  ballotfilemfp1  13280  ballotfilemic  13299  ennnfonelemk  13340  ennnfonelemhom  13355  ennnfonelemrnh  13356  ennnfonelemf1  13358  ctinf  13370  ctiunctlemudc  13377  ctiunctlemf  13378  nninfdclemp1  13390  strslfvd  13443  strslfv2d  13444  strslssd  13448  imasival  13676  imasbas  13677  imasplusg  13678  imasaddfnlemg  13684  imasaddvallemg  13685  qusaddvallemg  13703  qusaddflemg  13704  qusaddval  13705  qusaddf  13706  qusmulval  13707  qusmulf  13708  lidrididd  13751  gzsumfzval  13760  sgrpidmndm  13782  qusgrp2  13965  mulgnegnn  13984  eqgen  14079  rinvmod  14162  gzsumconst  14192  gsump1  14206  gsummptfidmadd  14210  qusrng  14306  srgdilem  14322  ringdilem  14365  qusring2  14420  lssintclm  14770  mplsubgfilemm  15138  eltg3  15207  iuncld  15265  cnss2  15377  txcnp  15421  uptx  15424  xblm  15567  metss  15644  fsumcncntop  15717  rescncf  15731  dedekindeulemlu  15771  suplociccex  15775  dedekindicclemlu  15780  dedekindicc  15783  ivthdec  15794  limccnp2lem  15826  dvaddxx  15853  dvmulxx  15854  dvrecap  15863  reeff1olem  15921  ppiqwordi  16174  ppiqeq0  16182  ppiqub  16194  perfectlem2  16198  lgsval  16221  lgsfvalg  16222  lgsfcl2  16223  lgscllem  16224  lgsval2lem  16227  lgsneg  16241  lgsdir2  16250  lgsdir  16252  lgsdi  16254  lgsne0  16255  lgsdirnn0  16264  lgsdinn0  16265  gausslemma2dlem0c  16268  m1lgs  16302  2lgslem1  16308  2lgs  16321  2lgsoddprm  16330  2sqlem6  16337  incistruhgr  16429  upgredg  16483  uhgr2edg  16545  usgriedgdomord  16564  wlkpropg  16663  wlkvtxeledgg  16683  wlk2f  16690  clwwlknonccat  16772  clwwlknonex2lem2  16777  eupth2lem3lem4fi  16812  eupth2lem3lem7fi  16813  dichmul0orlem3  16853  sumdc2  16925  pwle2  17126  subctctexmid  17128  nninfsellemeq  17155  nnnninfex  17163  exmidsbthrlem  17165  cndcap  17207