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  8588  lemulge11  8592  sup3exmid  8683  nngt0  8713  nn0ge0  8970  nn0ge2m1nn  9005  zletric  9066  zlelttric  9067  nn0n0n1ge2b  9098  nn0ind-raph  9136  supinfneg  9358  infsupneg  9359  rpge0  9422  fz0fzelfz0  9872  fz0fzdiffz0  9875  ige2m2fzo  9943  elfzodifsumelfzo  9946  elfzom1elp1fzo  9947  exfzdc  9985  qletric  9989  qlelttric  9990  rebtwn2zlemshrink  9999  frecuzrdgtcl  10153  frecuzrdg0  10154  frecuzrdgfunlem  10160  frecuzrdg0t  10163  frecuzrdgsuctlem  10164  frecfzennn  10167  seq3f1olemstep  10242  expcl2lemap  10273  leexp1a  10316  expnbnd  10383  faclbnd  10455  faclbnd6  10458  facavg  10460  fihasheqf1oi  10502  fihashf1rn  10503  fihashss  10530  seq3coll  10553  resqrexlemdecn  10752  qabsor  10815  cau3lem  10854  xrmaxiflemab  10984  xrmaxadd  10998  climcn2  11046  sumeq2  11096  sumrbdclem  11113  summodclem3  11117  summodclem2a  11118  zsumdc  11121  fsumgcl  11123  fsum3  11124  isumss  11128  fsumadd  11143  fsum2dlemstep  11171  fisum0diag2  11184  fsummulc2  11185  modfsummodlemstep  11194  fsumabs  11202  fsumrelem  11208  fsumiun  11214  isumshft  11227  mertenslem2  11273  sin02gt0  11397  efieq1re  11405  dvdsleabs2  11471  4dvdseven  11541  gcdmndc  11564  zsupcllemstep  11565  infssuzex  11569  gcdsupex  11573  gcdsupcl  11574  gcdeq0  11592  gcdaddm  11599  rppwr  11643  algfx  11660  eucalgcvga  11666  lcmmndc  11670  lcmval  11671  lcmcllem  11675  lcmledvds  11678  lcmeq0  11679  qredeq  11704  isprm3  11726  rpexp  11758  sqpweven  11780  2sqpwodd  11781  phicl2  11817  phibnd  11820  phiprmpw  11825  ennnfonelemk  11840  ennnfonelemhom  11855  ennnfonelemrnh  11856  ennnfonelemf1  11858  ctinf  11870  ctiunctlemudc  11877  ctiunctlemf  11878  strslfvd  11927  strslfv2d  11928  strslssd  11932  eltg3  12153  iuncld  12211  cnss2  12323  txcnp  12367  uptx  12370  xblm  12513  metss  12590  fsumcncntop  12652  rescncf  12664  dedekindeulemlu  12695  suplociccex  12699  dedekindicclemlu  12704  dedekindicc  12707  ivthdec  12718  limccnp2lem  12741  dvaddxx  12763  dvmulxx  12764  dvrecap  12773  sumdc2  12933  pwle2  13120  subctctexmid  13123  nninfalllemn  13129  nninfsellemeq  13137  exmidsbthrlem  13144
  Copyright terms: Public domain W3C validator