ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylc GIF 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 (𝜑𝜓)
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 49 1 (𝜑𝜃)
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  304  syl2anc  408  jc  639  jcnd  641  annimdc  921  orandc  923  dn1dc  944  syl2an23an  1277  xordidc  1377  nfimd  1564  exlimd2  1574  elex22  2701  elex2  2702  spcimdv  2770  spcimedv  2772  rspcdva  2794  elabd  2829  spsbcd  2921  opth  4162  euotd  4179  ssorduni  4406  tfisi  4504  omsinds  4538  nnpredcl  4539  sotri2  4939  sotri3  4940  unielrel  5069  funmo  5141  fnfvima  5655  fliftfun  5700  fliftval  5704  riota5f  5757  riotass2  5759  oprssdmm  6072  tfrlem5  6214  tfrlemibxssdm  6227  tfrlemibfn  6228  tfrlemiex  6231  tfr1onlemsucfn  6240  tfr1onlemsucaccv  6241  tfr1onlembxssdm  6243  tfr1onlembfn  6244  tfr1onlemex  6247  tfr1onlemres  6249  tfrcllemsucfn  6253  tfrcllemsucaccv  6254  tfrcllembxssdm  6256  tfrcllembfn  6257  tfrcllemex  6260  tfrcllemres  6262  tfrcl  6264  rdgisucinc  6285  frecabex  6298  frecabcl  6299  nntr2  6402  ertr  6447  qliftlem  6510  th3q  6537  resixp  6630  f1dom2g  6653  dom3d  6671  en1  6696  xpdom3m  6731  xpf1o  6741  phplem4dom  6759  phpm  6762  phpelm  6763  findcard  6785  finexdc  6799  fiintim  6820  fisseneq  6823  ssfirab  6825  f1dmvrnfibi  6835  iunfidisj  6837  fidcenumlemrk  6845  suplub2ti  6891  supelti  6892  ordiso2  6923  caseinl  6979  caseinr  6980  djudom  6981  difinfsn  6988  difinfinf  6989  ctm  6997  enumct  7003  ismkvnex  7032  exmidfodomrlemr  7070  exmidfodomrlemrALT  7071  acfun  7075  cc2lem  7093  cc3  7095  recexnq  7217  ltbtwnnqq  7242  addnnnq0  7276  mulnnnq0  7277  prarloclemn  7326  prarloc  7330  distrlem1prl  7409  distrlem1pru  7410  distrlem4prl  7411  distrlem4pru  7412  ltexprlemrl  7437  cauappcvgprlemladdru  7483  cauappcvgprlemladdrl  7484  addsrpr  7572  mulsrpr  7573  map2psrprg  7632  axpre-suploclemres  7728  lemul12a  8639  lemulge11  8643  sup3exmid  8734  nngt0  8764  nn0ge0  9021  nn0ge2m1nn  9056  zletric  9117  zlelttric  9118  nn0n0n1ge2b  9149  nn0ind-raph  9187  supinfneg  9412  infsupneg  9413  rpge0  9476  fz0fzelfz0  9928  fz0fzdiffz0  9931  ige2m2fzo  9999  elfzodifsumelfzo  10002  elfzom1elp1fzo  10003  exfzdc  10041  qletric  10045  qlelttric  10046  rebtwn2zlemshrink  10055  frecuzrdgtcl  10209  frecuzrdg0  10210  frecuzrdgfunlem  10216  frecuzrdg0t  10219  frecuzrdgsuctlem  10220  frecfzennn  10223  seq3f1olemstep  10298  expcl2lemap  10329  leexp1a  10372  expnbnd  10439  faclbnd  10511  faclbnd6  10514  facavg  10516  fihasheqf1oi  10558  fihashf1rn  10559  fihashss  10586  seq3coll  10609  resqrexlemdecn  10808  qabsor  10871  cau3lem  10910  xrmaxiflemab  11040  xrmaxadd  11054  climcn2  11102  sumeq2  11152  sumrbdclem  11170  summodclem3  11173  summodclem2a  11174  zsumdc  11177  fsumgcl  11179  fsum3  11180  isumss  11184  fsumadd  11199  fsum2dlemstep  11227  fisum0diag2  11240  fsummulc2  11241  modfsummodlemstep  11250  fsumabs  11258  fsumrelem  11264  fsumiun  11270  isumshft  11283  mertenslem2  11329  prodeq2  11350  prodrbdclem  11364  prodmodclem3  11368  prodmodclem2a  11369  sin02gt0  11493  efieq1re  11501  dvdsleabs2  11567  4dvdseven  11637  gcdmndc  11660  zsupcllemstep  11661  infssuzex  11665  gcdsupex  11669  gcdsupcl  11670  gcdeq0  11688  gcdaddm  11695  rppwr  11739  algfx  11756  eucalgcvga  11762  lcmmndc  11766  lcmval  11767  lcmcllem  11771  lcmledvds  11774  lcmeq0  11775  qredeq  11800  isprm3  11822  rpexp  11854  sqpweven  11876  2sqpwodd  11877  phicl2  11913  phibnd  11916  phiprmpw  11921  ennnfonelemk  11936  ennnfonelemhom  11951  ennnfonelemrnh  11952  ennnfonelemf1  11954  ctinf  11966  ctiunctlemudc  11973  ctiunctlemf  11974  strslfvd  12026  strslfv2d  12027  strslssd  12031  eltg3  12252  iuncld  12310  cnss2  12422  txcnp  12466  uptx  12469  xblm  12612  metss  12689  fsumcncntop  12751  rescncf  12763  dedekindeulemlu  12794  suplociccex  12798  dedekindicclemlu  12803  dedekindicc  12806  ivthdec  12817  limccnp2lem  12840  dvaddxx  12862  dvmulxx  12863  dvrecap  12872  reeff1olem  12887  sumdc2  13150  pwle2  13339  subctctexmid  13342  nninfalllemn  13350  nninfsellemeq  13358  exmidsbthrlem  13365
  Copyright terms: Public domain W3C validator