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

Theorem sylc 61
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 48 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  syl3c  62  mpsyl  64  imp  122  2thd  173  jca  300  syl2anc  403  jc  615  annimdc  883  orandc  885  dn1dc  906  syl2an23an  1235  xordidc  1335  nfimd  1522  exlimd2  1531  elex22  2634  elex2  2635  spcimdv  2703  spcimedv  2705  rspcdva  2727  spsbcd  2850  opth  4055  euotd  4072  ssorduni  4294  tfisi  4392  omsinds  4425  sotri2  4816  sotri3  4817  unielrel  4945  funmo  5017  fnfvima  5511  fliftfun  5557  fliftval  5561  riota5f  5614  riotass2  5616  tfrlem5  6061  tfrlemibxssdm  6074  tfrlemibfn  6075  tfrlemiex  6078  tfr1onlemsucfn  6087  tfr1onlemsucaccv  6088  tfr1onlembxssdm  6090  tfr1onlembfn  6091  tfr1onlemex  6094  tfr1onlemres  6096  tfrcllemsucfn  6100  tfrcllemsucaccv  6101  tfrcllembxssdm  6103  tfrcllembfn  6104  tfrcllemex  6107  tfrcllemres  6109  tfrcl  6111  rdgisucinc  6132  frecabex  6145  frecabcl  6146  ertr  6287  qliftlem  6350  th3q  6377  f1dom2g  6453  dom3d  6471  en1  6496  xpdom3m  6530  xpf1o  6540  phplem4dom  6558  phpm  6561  phpelm  6562  findcard  6584  finexdc  6598  fisseneq  6621  ssfirab  6622  f1dmvrnfibi  6632  iunfidisj  6634  fidcenumlemrk  6642  suplub2ti  6675  supelti  6676  ordiso2  6707  djudom  6766  exmidfodomrlemr  6807  exmidfodomrlemrALT  6808  recexnq  6928  ltbtwnnqq  6953  addnnnq0  6987  mulnnnq0  6988  prarloclemn  7037  prarloc  7041  distrlem1prl  7120  distrlem1pru  7121  distrlem4prl  7122  distrlem4pru  7123  ltexprlemrl  7148  cauappcvgprlemladdru  7194  cauappcvgprlemladdrl  7195  addsrpr  7270  mulsrpr  7271  lemul12a  8295  lemulge11  8299  nngt0  8419  nn0ge0  8668  nn0ge2m1nn  8703  zletric  8764  zlelttric  8765  nn0n0n1ge2b  8796  nn0ind-raph  8833  supinfneg  9052  infsupneg  9053  rpge0  9115  fz0fzelfz0  9503  fz0fzdiffz0  9506  ige2m2fzo  9574  elfzodifsumelfzo  9577  elfzom1elp1fzo  9578  exfzdc  9616  qletric  9620  qlelttric  9621  rebtwn2zlemshrink  9630  frecuzrdgtcl  9784  frecuzrdg0  9785  frecuzrdgfunlem  9791  frecuzrdg0t  9794  frecuzrdgsuctlem  9795  frecfzennn  9798  seq3f1olemstep  9895  expcl2lemap  9932  leexp1a  9975  expnbnd  10042  faclbnd  10114  faclbnd6  10117  facavg  10119  fihasheqf1oi  10161  fihashf1rn  10162  fihashss  10189  iseqcoll  10212  resqrexlemdecn  10410  qabsor  10473  cau3lem  10512  climcn2  10662  sumeq2  10712  isumrblem  10729  isummolem3  10734  isummolem2a  10735  zisum  10738  fsumgcl  10741  fisum  10742  isumss  10747  fsumadd  10763  isummulc2  10783  fsum2dlemstep  10791  fisum0diag2  10804  fsummulc2  10805  modfsummodlemstep  10814  fsumabs  10822  fsumrelem  10828  fsumiun  10833  isumshft  10846  dvdsleabs2  10940  4dvdseven  11010  gcdmndc  11033  zsupcllemstep  11034  infssuzex  11038  gcdsupex  11042  gcdsupcl  11043  gcdeq0  11061  gcdaddm  11068  rppwr  11110  ialgfx  11127  eucialgcvga  11133  lcmmndc  11137  lcmval  11138  lcmcllem  11142  lcmledvds  11145  lcmeq0  11146  qredeq  11171  isprm3  11193  rpexp  11225  sqpweven  11246  2sqpwodd  11247  phicl2  11283  phibnd  11286  phiprmpw  11291  sumdc2  11356  nnpredcl  11547  nninfalllemn  11555  nninfsellemeq  11563  exmidsbthrlem  11569
  Copyright terms: Public domain W3C validator