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

Theorem sylancr 411
Description: Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)
Hypotheses
Ref Expression
sylancr.1  |-  ps
sylancr.2  |-  ( ph  ->  ch )
sylancr.3  |-  ( ( ps  /\  ch )  ->  th )
Assertion
Ref Expression
sylancr  |-  ( ph  ->  th )

Proof of Theorem sylancr
StepHypRef Expression
1 sylancr.1 . . 3  |-  ps
21a1i 9 . 2  |-  ( ph  ->  ps )
3 sylancr.2 . 2  |-  ( ph  ->  ch )
4 sylancr.3 . 2  |-  ( ( ps  /\  ch )  ->  th )
52, 3, 4syl2anc 409 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107
This theorem is referenced by:  mpteq2da  4024  unipw  4146  opeluu  4378  uniexb  4401  unon  4434  onintrab2im  4441  xpexg  4660  resiexg  4871  imaexg  4900  exse2  4920  soirri  4940  djudisj  4973  elxp5  5034  cnvexg  5083  cnviinm  5087  coexg  5090  funssres  5172  f1oabexg  5386  sefvex  5449  ssimaex  5489  mptfvex  5513  f1ompt  5578  fmptcof  5594  resfunexg  5648  mptexg  5652  funfvima3  5658  ovid  5894  ov  5897  ofres  6003  cofunexg  6016  opabex3d  6026  opabex3  6027  oprabexd  6032  1stcof  6068  2ndcof  6069  mpoexxg  6115  cnvf1o  6129  f2ndf  6130  algrflemg  6134  tposexg  6162  tfrlemisucaccv  6229  tfrlemibxssdm  6231  tfrlemibfn  6232  tfrlemi14d  6237  tfr1onlemsucaccv  6245  tfr1onlembxssdm  6247  tfr1onlembfn  6248  tfr1onlemres  6253  tfrcllemsucaccv  6258  tfrcllembxssdm  6260  tfrcllembfn  6261  tfrcllemres  6266  rdgtfr  6278  rdgruledefgg  6279  rdgon  6290  frecabex  6302  freccllem  6306  frecfcllem  6308  omcl  6364  oeicl  6365  erth  6480  th3qlem1  6538  mapex  6555  pmvalg  6560  mapsnconst  6595  ixpexgg  6623  fundmen  6707  cnvct  6710  snfig  6715  unen  6717  xpdom2  6732  mapxpen  6749  phplem2  6754  findcard2  6790  findcard2s  6791  infnfi  6796  relcnvfi  6836  sbthlemi8  6859  sbthlemi10  6861  fival  6865  fiss  6872  inl11  6957  casef  6980  caseinj  6981  caseinl  6983  caseinr  6984  djudom  6985  difinfsn  6992  djuinj  6998  0ct  6999  ctmlemr  7000  ctssdccl  7003  enomnilem  7017  enmkvlem  7042  enwomnilem  7049  djuassen  7089  xpdjuen  7090  djudoml  7091  djudomr  7092  cc2lem  7097  ltnnnq  7254  nnnq0lem1  7277  addnqprlemfl  7390  addnqprlemfu  7391  mulnqprlemfl  7406  mulnqprlemfu  7407  suplocexprlem2b  7545  prsrlem1  7573  gt0srpr  7579  caucvgsrlemcl  7620  caucvgsrlemfv  7622  caucvgsrlembound  7625  mulcnsr  7666  mulcnsrec  7674  addvalex  7675  pitoregt0  7680  axmulass  7704  axdistr  7705  recriota  7721  mulid1  7786  axmulgt0  7859  cnegexlem2  7961  cnegex  7963  gt0ne0d  8297  recexre  8363  msqge0  8401  mulge0  8404  recgt0  8631  recreclt  8681  cju  8742  nnge1  8766  nnnlt1  8769  nn0nlt0  9026  elz2  9145  nnm1ge0  9160  recnz  9167  zneo  9175  uz3m2nn  9394  eluz2b2  9423  nn01to3  9435  mnflt  9598  xltadd1  9688  lincmb01cmp  9815  iccf1o  9816  fz1n  9854  fseq1p1m1  9904  fznn0  9923  fzctr  9940  4fvwrd4  9947  elfzonlteqm1  10017  divfl0  10099  modqelico  10137  zmodfz  10149  modqid  10152  modqmuladdim  10170  m1modge3gt1  10174  addmodid  10175  frec2uzf1od  10209  frecfzennn  10229  frecfzen2  10230  fzfig  10233  ser0  10317  ser3le  10321  expgt1  10361  expubnd  10380  iexpcyc  10427  binom2sub  10435  binom3  10439  zesq  10440  bernneq  10442  bernneq2  10443  expnbnd  10445  expnlbnd2  10447  facdiv  10515  faclbnd2  10519  faclbnd3  10520  bcval4  10529  hashinfom  10555  hashennn  10557  fihashf1rn  10566  isfinite4im  10570  hashfz  10598  crre  10660  crim  10661  remim  10663  mulreap  10667  cjreb  10669  recj  10670  reneg  10671  readd  10672  remullem  10674  imcj  10678  imneg  10679  imadd  10680  cjadd  10687  cjneg  10693  imval2  10697  cjreim  10706  cnrecnv  10713  uzin2  10790  absval  10804  rennim  10805  resqrexlemcalc3  10819  resqrexlemnm  10821  resqrexlemcvg  10822  resqrexlemgt0  10823  resqrexlemga  10826  absreimsq  10870  absreim  10871  amgm2  10921  climconst2  11091  climshft  11104  climshft2  11106  reccn2ap  11113  climge0  11125  sumsnf  11209  sumnul  11224  isumcl  11225  fsum2dlemstep  11234  fisumcom2  11238  fsumabs  11265  fsumiun  11277  binom  11284  bcxmas  11289  arisum  11298  expcnvap0  11302  explecnv  11305  geosergap  11306  geolim  11311  geolim2  11312  geo2sum  11314  geo2lim  11316  cvgratnnlemrate  11330  cvgratz  11332  mertenslemi1  11335  prodf1  11342  prodeq2w  11356  efcllemp  11399  ege2le3  11412  eftlub  11431  efgt1  11438  tanval2ap  11454  tanval3ap  11455  resinval  11456  recosval  11457  efi4p  11458  resin4p  11459  recos4p  11460  resincl  11461  recoscl  11462  efmival  11474  efeul  11475  sinadd  11477  cosadd  11478  tanaddap  11480  sinmul  11485  cos2tsin  11492  ef01bndlem  11497  sin01bnd  11498  cos01bnd  11499  sin01gt0  11502  cos01gt0  11503  absef  11510  absefib  11511  efieq1re  11512  demoivreALT  11514  eirraplem  11517  odd2np1  11604  oddm1even  11606  oddp1even  11607  oexpneg  11608  opoe  11626  omoe  11627  nn0o1gt2  11636  nn0o  11638  algcvg  11763  algcvgblem  11764  1nprm  11829  1idssfct  11830  oddprmge3  11849  divgcdodd  11855  pw2dvdslemn  11877  pw2dvds  11878  oddpwdclemodd  11884  oddpwdc  11886  phicl2  11924  phibndlem  11926  phibnd  11927  hashdvds  11931  crth  11934  phimullem  11935  hashgcdeq  11938  evenennn  11940  ennnfonelemj0  11948  ennnfonelemjn  11949  ennnfonelemg  11950  ennnfonelemkh  11959  ennnfonelemhf1o  11960  ennnfonelemex  11961  ennnfonelemhom  11962  ennnfonelemnn0  11969  exmidunben  11973  ctinfomlemom  11974  slotex  12023  setscom  12036  setsslid  12046  2strbas1g  12100  2strop1g  12101  rngbaseg  12112  rngplusgg  12113  rngmulrg  12114  srngbased  12119  srngplusgd  12120  srngmulrd  12121  srnginvld  12122  lmodbased  12130  lmodplusgd  12131  lmodscad  12132  lmodvscad  12133  ipsbased  12138  ipsaddgd  12139  ipsmulrd  12140  ipsscad  12141  ipsvscad  12142  ipsipd  12143  topgrpbasd  12148  topgrpplusgd  12149  topgrptsetd  12150  toponsspwpwg  12226  topgele  12233  istps  12236  topontopn  12241  tgvalex  12256  tgclb  12271  lmfval  12398  lmres  12454  ispsmet  12529  psmetge0  12537  ismet  12550  isxmet  12551  xmetge0  12571  isxms2  12658  comet  12705  bdxmet  12707  cnmetdval  12735  cnbl0  12740  cnblcld  12741  reopnap  12744  tgioo  12752  cncfcncntop  12786  cncfmpt2fcntop  12791  limcimolemlt  12839  cnplimcim  12842  cnplimclemr  12844  limccnpcntop  12850  limccnp2lem  12851  limccnp2cntop  12852  dvfvalap  12856  dvbss  12860  dvcnp2cntop  12869  dvcn  12870  dvaddxxbr  12871  dvmulxxbr  12872  dvcoapbr  12877  dvcjbr  12878  dvrecap  12883  dveflem  12893  reeff1olem  12898  pilem3  12910  ef2kpi  12933  efper  12934  sinperlem  12935  efimpi  12946  ptolemy  12951  sincosq2sgn  12954  sincosq3sgn  12955  sincosq4sgn  12956  sinq12gt0  12957  cosq14gt0  12959  tangtx  12965  sinkpi  12974  coskpi  12975  cosordlem  12976  rplogcl  13006  logge0  13007  logdivlti  13008  logbleb  13084  logblt  13085  pwf1oexmid  13365  isomninnlem  13398  iswomninnlem  13415  ismkvnnlem  13417
  Copyright terms: Public domain W3C validator