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

Theorem sylc 56
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
StepHypRef Expression
1 sylc.1 . . 3 (𝜑𝜓)
2 sylc.2 . . 3 (𝜑𝜒)
3 sylc.3 . . 3 (𝜓 → (𝜒𝜃))
41, 2, 3syl2im 34 . 2 (𝜑 → (𝜑𝜃))
54pm2.43i 43 1 (𝜑𝜃)
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  57  mpsyl  59  imp  115  2thd  164  jca  290  syl2anc  391  jc  580  annimdc  845  dn1dc  867  xordidc  1290  nfimd  1477  exlimd2  1486  elex22  2569  elex2  2570  spcimdv  2637  spcimedv  2639  spsbcd  2776  opth  3974  euotd  3991  ssorduni  4213  wetriext  4301  tfisi  4310  sotri2  4722  sotri3  4723  unielrel  4845  funmo  4917  fnfvima  5393  fliftfun  5436  fliftval  5440  riota5f  5492  riotass2  5494  grprinvlem  5695  grprinvd  5696  caofref  5732  tfrlem1  5923  tfrlem5  5930  tfrlemibxssdm  5941  tfrlemibfn  5942  tfrlemiex  5945  rdgisucinc  5972  frecabex  5984  ertr  6121  qliftlem  6184  th3q  6211  f1dom2g  6236  dom3d  6254  en1  6279  xpdom3m  6308  phplem4dom  6324  phpm  6327  phpelm  6328  findcard  6345  ordiso2  6355  recexnq  6486  ltbtwnnqq  6511  addnnnq0  6545  mulnnnq0  6546  prltlu  6583  prarloclemn  6595  prarloc  6599  distrlem1prl  6678  distrlem1pru  6679  distrlem4prl  6680  distrlem4pru  6681  ltexprlemrl  6706  cauappcvgprlemladdru  6752  cauappcvgprlemladdrl  6753  caucvgprprlemml  6790  addsrpr  6828  mulsrpr  6829  axcaucvglemres  6971  lemul12a  7826  lemulge11  7830  nngt0  7937  nn0ge0  8205  nn0ge2m1nn  8240  zletric  8287  zlelttric  8288  nn0n0n1ge2b  8318  nn0ind-raph  8353  rpge0  8593  fz0fzelfz0  8982  fz0fzdiffz0  8985  ige2m2fzo  9052  elfzodifsumelfzo  9055  elfzom1elp1fzo  9056  qletric  9097  qlelttric  9098  qbtwnzlemshrink  9102  rebtwn2zlemshrink  9106  frecuzrdgfn  9196  frecuzrdg0  9198  frecfzennn  9201  iseqovex  9217  iseqfn  9219  iseq1  9220  iseqcl  9221  iseqp1  9223  iseqfveq2  9226  iseqfveq  9228  iseqshft2  9230  monoord  9233  monoord2  9234  isermono  9235  iseqsplit  9236  iseqcaopr3  9238  iseqid3s  9244  iseqid  9245  iseqhomo  9246  expcl2lemap  9265  leexp1a  9307  expnbnd  9370  cvg1nlemcau  9581  cvg1nlemres  9582  recvguniq  9591  resqrexlemdecn  9608  resqrexlemgt0  9616  resqrexlemoverl  9617  resqrexlemglsq  9618  cau3lem  9708  climi  9806  climcn1  9827  climcn2  9828  ialgfx  9889
  Copyright terms: Public domain W3C validator