ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylc Unicode version

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  |-  ( ph  ->  ps )
sylc.2  |-  ( ph  ->  ch )
sylc.3  |-  ( ps 
->  ( ch  ->  th )
)
Assertion
Ref Expression
sylc  |-  ( ph  ->  th )

Proof of Theorem sylc
StepHypRef Expression
1 sylc.1 . . 3  |-  ( ph  ->  ps )
2 sylc.2 . . 3  |-  ( ph  ->  ch )
3 sylc.3 . . 3  |-  ( ps 
->  ( ch  ->  th )
)
41, 2, 3syl2im 38 . 2  |-  ( ph  ->  ( ph  ->  th )
)
54pm2.43i 49 1  |-  ( ph  ->  th )
Colors of variables: wff set class
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  302  syl2anc  406  jc  623  annimdc  904  orandc  906  dn1dc  927  syl2an23an  1260  xordidc  1360  nfimd  1547  exlimd2  1557  elex22  2673  elex2  2674  spcimdv  2742  spcimedv  2744  rspcdva  2766  spsbcd  2892  opth  4127  euotd  4144  ssorduni  4371  tfisi  4469  omsinds  4503  nnpredcl  4504  sotri2  4904  sotri3  4905  unielrel  5034  funmo  5106  fnfvima  5618  fliftfun  5663  fliftval  5667  riota5f  5720  riotass2  5722  oprssdmm  6035  tfrlem5  6177  tfrlemibxssdm  6190  tfrlemibfn  6191  tfrlemiex  6194  tfr1onlemsucfn  6203  tfr1onlemsucaccv  6204  tfr1onlembxssdm  6206  tfr1onlembfn  6207  tfr1onlemex  6210  tfr1onlemres  6212  tfrcllemsucfn  6216  tfrcllemsucaccv  6217  tfrcllembxssdm  6219  tfrcllembfn  6220  tfrcllemex  6223  tfrcllemres  6225  tfrcl  6227  rdgisucinc  6248  frecabex  6261  frecabcl  6262  nntr2  6365  ertr  6410  qliftlem  6473  th3q  6500  resixp  6593  f1dom2g  6616  dom3d  6634  en1  6659  xpdom3m  6694  xpf1o  6704  phplem4dom  6722  phpm  6725  phpelm  6726  findcard  6748  finexdc  6762  fiintim  6783  fisseneq  6786  ssfirab  6788  f1dmvrnfibi  6798  iunfidisj  6800  fidcenumlemrk  6808  suplub2ti  6854  supelti  6855  ordiso2  6886  caseinl  6942  caseinr  6943  djudom  6944  difinfsn  6951  difinfinf  6952  ctm  6960  enumct  6966  ismkvnex  6995  exmidfodomrlemr  7022  exmidfodomrlemrALT  7023  acfun  7027  recexnq  7162  ltbtwnnqq  7187  addnnnq0  7221  mulnnnq0  7222  prarloclemn  7271  prarloc  7275  distrlem1prl  7354  distrlem1pru  7355  distrlem4prl  7356  distrlem4pru  7357  ltexprlemrl  7382  cauappcvgprlemladdru  7428  cauappcvgprlemladdrl  7429  addsrpr  7517  mulsrpr  7518  map2psrprg  7577  axpre-suploclemres  7673  lemul12a  8580  lemulge11  8584  sup3exmid  8675  nngt0  8705  nn0ge0  8956  nn0ge2m1nn  8991  zletric  9052  zlelttric  9053  nn0n0n1ge2b  9084  nn0ind-raph  9122  supinfneg  9342  infsupneg  9343  rpge0  9405  fz0fzelfz0  9855  fz0fzdiffz0  9858  ige2m2fzo  9926  elfzodifsumelfzo  9929  elfzom1elp1fzo  9930  exfzdc  9968  qletric  9972  qlelttric  9973  rebtwn2zlemshrink  9982  frecuzrdgtcl  10136  frecuzrdg0  10137  frecuzrdgfunlem  10143  frecuzrdg0t  10146  frecuzrdgsuctlem  10147  frecfzennn  10150  seq3f1olemstep  10225  expcl2lemap  10256  leexp1a  10299  expnbnd  10366  faclbnd  10438  faclbnd6  10441  facavg  10443  fihasheqf1oi  10485  fihashf1rn  10486  fihashss  10513  seq3coll  10536  resqrexlemdecn  10735  qabsor  10798  cau3lem  10837  xrmaxiflemab  10967  xrmaxadd  10981  climcn2  11029  sumeq2  11079  sumrbdclem  11096  summodclem3  11100  summodclem2a  11101  zsumdc  11104  fsumgcl  11106  fsum3  11107  isumss  11111  fsumadd  11126  fsum2dlemstep  11154  fisum0diag2  11167  fsummulc2  11168  modfsummodlemstep  11177  fsumabs  11185  fsumrelem  11191  fsumiun  11197  isumshft  11210  mertenslem2  11256  sin02gt0  11380  efieq1re  11387  dvdsleabs2  11451  4dvdseven  11521  gcdmndc  11544  zsupcllemstep  11545  infssuzex  11549  gcdsupex  11553  gcdsupcl  11554  gcdeq0  11572  gcdaddm  11579  rppwr  11623  algfx  11640  eucalgcvga  11646  lcmmndc  11650  lcmval  11651  lcmcllem  11655  lcmledvds  11658  lcmeq0  11659  qredeq  11684  isprm3  11706  rpexp  11738  sqpweven  11759  2sqpwodd  11760  phicl2  11796  phibnd  11799  phiprmpw  11804  ennnfonelemk  11819  ennnfonelemhom  11834  ennnfonelemrnh  11835  ennnfonelemf1  11837  ctinf  11849  ctiunctlemudc  11856  ctiunctlemf  11857  strslfvd  11906  strslfv2d  11907  strslssd  11911  eltg3  12132  iuncld  12190  cnss2  12302  txcnp  12346  uptx  12349  xblm  12492  metss  12569  fsumcncntop  12631  rescncf  12643  dedekindeulemlu  12674  suplociccex  12678  dedekindicclemlu  12683  dedekindicc  12686  ivthdec  12697  limccnp2lem  12720  dvaddxx  12742  dvmulxx  12743  dvrecap  12752  sumdc2  12840  pwle2  13027  subctctexmid  13030  nninfalllemn  13036  nninfsellemeq  13044  exmidsbthrlem  13051
  Copyright terms: Public domain W3C validator