ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sylc Unicode 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  |-  ( 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 49 1  |-  ( ph  ->  th )
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  625  annimdc  906  orandc  908  dn1dc  929  syl2an23an  1262  xordidc  1362  nfimd  1549  exlimd2  1559  elex22  2675  elex2  2676  spcimdv  2744  spcimedv  2746  rspcdva  2768  spsbcd  2894  opth  4129  euotd  4146  ssorduni  4373  tfisi  4471  omsinds  4505  nnpredcl  4506  sotri2  4906  sotri3  4907  unielrel  5036  funmo  5108  fnfvima  5620  fliftfun  5665  fliftval  5669  riota5f  5722  riotass2  5724  oprssdmm  6037  tfrlem5  6179  tfrlemibxssdm  6192  tfrlemibfn  6193  tfrlemiex  6196  tfr1onlemsucfn  6205  tfr1onlemsucaccv  6206  tfr1onlembxssdm  6208  tfr1onlembfn  6209  tfr1onlemex  6212  tfr1onlemres  6214  tfrcllemsucfn  6218  tfrcllemsucaccv  6219  tfrcllembxssdm  6221  tfrcllembfn  6222  tfrcllemex  6225  tfrcllemres  6227  tfrcl  6229  rdgisucinc  6250  frecabex  6263  frecabcl  6264  nntr2  6367  ertr  6412  qliftlem  6475  th3q  6502  resixp  6595  f1dom2g  6618  dom3d  6636  en1  6661  xpdom3m  6696  xpf1o  6706  phplem4dom  6724  phpm  6727  phpelm  6728  findcard  6750  finexdc  6764  fiintim  6785  fisseneq  6788  ssfirab  6790  f1dmvrnfibi  6800  iunfidisj  6802  fidcenumlemrk  6810  suplub2ti  6856  supelti  6857  ordiso2  6888  caseinl  6944  caseinr  6945  djudom  6946  difinfsn  6953  difinfinf  6954  ctm  6962  enumct  6968  ismkvnex  6997  exmidfodomrlemr  7026  exmidfodomrlemrALT  7027  acfun  7031  recexnq  7166  ltbtwnnqq  7191  addnnnq0  7225  mulnnnq0  7226  prarloclemn  7275  prarloc  7279  distrlem1prl  7358  distrlem1pru  7359  distrlem4prl  7360  distrlem4pru  7361  ltexprlemrl  7386  cauappcvgprlemladdru  7432  cauappcvgprlemladdrl  7433  addsrpr  7521  mulsrpr  7522  map2psrprg  7581  axpre-suploclemres  7677  lemul12a  8584  lemulge11  8588  sup3exmid  8679  nngt0  8709  nn0ge0  8960  nn0ge2m1nn  8995  zletric  9056  zlelttric  9057  nn0n0n1ge2b  9088  nn0ind-raph  9126  supinfneg  9346  infsupneg  9347  rpge0  9409  fz0fzelfz0  9859  fz0fzdiffz0  9862  ige2m2fzo  9930  elfzodifsumelfzo  9933  elfzom1elp1fzo  9934  exfzdc  9972  qletric  9976  qlelttric  9977  rebtwn2zlemshrink  9986  frecuzrdgtcl  10140  frecuzrdg0  10141  frecuzrdgfunlem  10147  frecuzrdg0t  10150  frecuzrdgsuctlem  10151  frecfzennn  10154  seq3f1olemstep  10229  expcl2lemap  10260  leexp1a  10303  expnbnd  10370  faclbnd  10442  faclbnd6  10445  facavg  10447  fihasheqf1oi  10489  fihashf1rn  10490  fihashss  10517  seq3coll  10540  resqrexlemdecn  10739  qabsor  10802  cau3lem  10841  xrmaxiflemab  10971  xrmaxadd  10985  climcn2  11033  sumeq2  11083  sumrbdclem  11100  summodclem3  11104  summodclem2a  11105  zsumdc  11108  fsumgcl  11110  fsum3  11111  isumss  11115  fsumadd  11130  fsum2dlemstep  11158  fisum0diag2  11171  fsummulc2  11172  modfsummodlemstep  11181  fsumabs  11189  fsumrelem  11195  fsumiun  11201  isumshft  11214  mertenslem2  11260  sin02gt0  11384  efieq1re  11392  dvdsleabs2  11456  4dvdseven  11526  gcdmndc  11549  zsupcllemstep  11550  infssuzex  11554  gcdsupex  11558  gcdsupcl  11559  gcdeq0  11577  gcdaddm  11584  rppwr  11628  algfx  11645  eucalgcvga  11651  lcmmndc  11655  lcmval  11656  lcmcllem  11660  lcmledvds  11663  lcmeq0  11664  qredeq  11689  isprm3  11711  rpexp  11743  sqpweven  11764  2sqpwodd  11765  phicl2  11801  phibnd  11804  phiprmpw  11809  ennnfonelemk  11824  ennnfonelemhom  11839  ennnfonelemrnh  11840  ennnfonelemf1  11842  ctinf  11854  ctiunctlemudc  11861  ctiunctlemf  11862  strslfvd  11911  strslfv2d  11912  strslssd  11916  eltg3  12137  iuncld  12195  cnss2  12307  txcnp  12351  uptx  12354  xblm  12497  metss  12574  fsumcncntop  12636  rescncf  12648  dedekindeulemlu  12679  suplociccex  12683  dedekindicclemlu  12688  dedekindicc  12691  ivthdec  12702  limccnp2lem  12725  dvaddxx  12747  dvmulxx  12748  dvrecap  12757  sumdc2  12902  pwle2  13089  subctctexmid  13092  nninfalllemn  13098  nninfsellemeq  13106  exmidsbthrlem  13113
  Copyright terms: Public domain W3C validator