ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylc GIF 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 (𝜑𝜓)
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 38 . 2 (𝜑 → (𝜑𝜃))
54pm2.43i 48 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  62  mpsyl  64  imp  122  2thd  173  jca  300  syl2anc  403  jc  613  annimdc  881  orandc  883  dn1dc  904  syl2an23an  1233  xordidc  1333  nfimd  1520  exlimd2  1529  elex22  2628  elex2  2629  spcimdv  2696  spcimedv  2698  rspcdva  2720  spsbcd  2841  opth  4038  euotd  4055  ssorduni  4277  tfisi  4375  omsinds  4408  sotri2  4796  sotri3  4797  unielrel  4924  funmo  4996  fnfvima  5490  fliftfun  5536  fliftval  5540  riota5f  5593  riotass2  5595  tfrlem5  6033  tfrlemibxssdm  6046  tfrlemibfn  6047  tfrlemiex  6050  tfr1onlemsucfn  6059  tfr1onlemsucaccv  6060  tfr1onlembxssdm  6062  tfr1onlembfn  6063  tfr1onlemex  6066  tfr1onlemres  6068  tfrcllemsucfn  6072  tfrcllemsucaccv  6073  tfrcllembxssdm  6075  tfrcllembfn  6076  tfrcllemex  6079  tfrcllemres  6081  tfrcl  6083  rdgisucinc  6104  frecabex  6117  frecabcl  6118  ertr  6259  qliftlem  6322  th3q  6349  f1dom2g  6425  dom3d  6443  en1  6468  xpdom3m  6502  xpf1o  6512  phplem4dom  6530  phpm  6533  phpelm  6534  findcard  6556  finexdc  6570  fisseneq  6592  ssfirab  6593  f1dmvrnfibi  6603  suplub2ti  6640  supelti  6641  ordiso2  6672  djudom  6731  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  recexnq  6893  ltbtwnnqq  6918  addnnnq0  6952  mulnnnq0  6953  prarloclemn  7002  prarloc  7006  distrlem1prl  7085  distrlem1pru  7086  distrlem4prl  7087  distrlem4pru  7088  ltexprlemrl  7113  cauappcvgprlemladdru  7159  cauappcvgprlemladdrl  7160  addsrpr  7235  mulsrpr  7236  lemul12a  8258  lemulge11  8262  nngt0  8382  nn0ge0  8631  nn0ge2m1nn  8666  zletric  8727  zlelttric  8728  nn0n0n1ge2b  8759  nn0ind-raph  8796  supinfneg  9015  infsupneg  9016  rpge0  9078  fz0fzelfz0  9466  fz0fzdiffz0  9469  ige2m2fzo  9537  elfzodifsumelfzo  9540  elfzom1elp1fzo  9541  exfzdc  9579  qletric  9583  qlelttric  9584  rebtwn2zlemshrink  9593  frecuzrdgtcl  9747  frecuzrdg0  9748  frecuzrdgfunlem  9754  frecuzrdg0t  9757  frecuzrdgsuctlem  9758  frecfzennn  9761  iseqf1olemstep  9835  expcl2lemap  9866  leexp1a  9909  expnbnd  9974  faclbnd  10046  faclbnd6  10049  facavg  10051  fihasheqf1oi  10093  fihashf1rn  10094  fihashss  10121  iseqcoll  10144  resqrexlemdecn  10341  qabsor  10404  cau3lem  10443  climcn2  10592  sumeq2  10640  isumrblem  10657  isummolem3  10661  isummolem2a  10662  zisum  10665  fisum  10667  isumss  10671  dvdsleabs2  10729  4dvdseven  10799  gcdmndc  10822  zsupcllemstep  10823  infssuzex  10827  gcdsupex  10831  gcdsupcl  10832  gcdeq0  10850  gcdaddm  10857  rppwr  10899  ialgfx  10916  eucialgcvga  10922  lcmmndc  10926  lcmval  10927  lcmcllem  10931  lcmledvds  10934  lcmeq0  10935  qredeq  10960  isprm3  10982  rpexp  11014  sqpweven  11035  2sqpwodd  11036  phicl2  11072  phibnd  11075  phiprmpw  11080  sumdc2  11144  nnpredcl  11335  nninfalllemn  11343  nninfsellemeq  11351  exmidsbthrlem  11357
  Copyright terms: Public domain W3C validator