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

Theorem sylc 60
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 47 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  61  mpsyl  63  imp  119  2thd  168  jca  294  syl2anc  397  jc  590  annimdc  856  dn1dc  878  xordidc  1306  nfimd  1493  exlimd2  1502  elex22  2586  elex2  2587  spcimdv  2654  spcimedv  2656  rspcda  2678  spsbcd  2799  opth  4002  euotd  4019  ssorduni  4241  wetriext  4329  tfisi  4338  sotri2  4750  sotri3  4751  unielrel  4873  funmo  4945  fnfvima  5421  fliftfun  5464  fliftval  5468  riota5f  5520  riotass2  5522  grprinvlem  5723  grprinvd  5724  caofref  5760  tfrlem1  5954  tfrlem5  5961  tfrlemibxssdm  5972  tfrlemibfn  5973  tfrlemiex  5976  rdgisucinc  6003  frecabex  6015  ertr  6152  qliftlem  6215  th3q  6242  f1dom2g  6267  dom3d  6285  en1  6310  xpdom3m  6339  phplem4dom  6355  phpm  6358  phpelm  6359  findcard  6376  ordiso2  6415  recexnq  6546  ltbtwnnqq  6571  addnnnq0  6605  mulnnnq0  6606  prltlu  6643  prarloclemn  6655  prarloc  6659  distrlem1prl  6738  distrlem1pru  6739  distrlem4prl  6740  distrlem4pru  6741  ltexprlemrl  6766  cauappcvgprlemladdru  6812  cauappcvgprlemladdrl  6813  caucvgprprlemml  6850  addsrpr  6888  mulsrpr  6889  axcaucvglemres  7031  lemul12a  7903  lemulge11  7907  nngt0  8015  nn0ge0  8264  nn0ge2m1nn  8299  zletric  8346  zlelttric  8347  nn0n0n1ge2b  8378  nn0ind-raph  8414  rpge0  8693  fz0fzelfz0  9086  fz0fzdiffz0  9089  ige2m2fzo  9156  elfzodifsumelfzo  9159  elfzom1elp1fzo  9160  qletric  9201  qlelttric  9202  qbtwnzlemshrink  9206  rebtwn2zlemshrink  9210  frecuzrdgfn  9362  frecuzrdg0  9364  frecfzennn  9367  iseqovex  9383  iseqfn  9385  iseq1  9386  iseqcl  9387  iseqp1  9389  iseqfveq2  9392  iseqfveq  9394  iseqshft2  9396  monoord  9399  monoord2  9400  isermono  9401  iseqsplit  9402  iseqcaopr3  9404  iseqid3s  9410  iseqid  9411  iseqhomo  9412  expcl2lemap  9432  leexp1a  9475  expnbnd  9540  faclbnd  9609  faclbnd6  9612  facavg  9614  cvg1nlemcau  9811  cvg1nlemres  9812  recvguniq  9822  resqrexlemdecn  9839  resqrexlemgt0  9847  resqrexlemoverl  9848  resqrexlemglsq  9849  qabsor  9902  cau3lem  9941  climi  10039  climcn1  10060  climcn2  10061  dvdsleabs2  10158  4dvdseven  10229  ialgfx  10274
  Copyright terms: Public domain W3C validator