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

Theorem sylancr 410
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 408 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  3987  unipw  4109  opeluu  4341  uniexb  4364  unon  4397  onintrab2im  4404  xpexg  4623  resiexg  4834  imaexg  4863  exse2  4883  soirri  4903  djudisj  4936  elxp5  4997  cnvexg  5046  cnviinm  5050  coexg  5053  funssres  5135  f1oabexg  5347  sefvex  5410  ssimaex  5450  mptfvex  5474  f1ompt  5539  fmptcof  5555  resfunexg  5609  mptexg  5613  funfvima3  5619  ovid  5855  ov  5858  ofres  5964  cofunexg  5977  opabex3d  5987  opabex3  5988  oprabexd  5993  1stcof  6029  2ndcof  6030  mpoexxg  6076  cnvf1o  6090  f2ndf  6091  algrflemg  6095  tposexg  6123  tfrlemisucaccv  6190  tfrlemibxssdm  6192  tfrlemibfn  6193  tfrlemi14d  6198  tfr1onlemsucaccv  6206  tfr1onlembxssdm  6208  tfr1onlembfn  6209  tfr1onlemres  6214  tfrcllemsucaccv  6219  tfrcllembxssdm  6221  tfrcllembfn  6222  tfrcllemres  6227  rdgtfr  6239  rdgruledefgg  6240  rdgon  6251  frecabex  6263  freccllem  6267  frecfcllem  6269  omcl  6325  oeicl  6326  erth  6441  th3qlem1  6499  mapex  6516  pmvalg  6521  mapsnconst  6556  ixpexgg  6584  fundmen  6668  cnvct  6671  snfig  6676  unen  6678  xpdom2  6693  mapxpen  6710  phplem2  6715  findcard2  6751  findcard2s  6752  infnfi  6757  relcnvfi  6797  sbthlemi8  6820  sbthlemi10  6822  fival  6826  fiss  6833  inl11  6918  casef  6941  caseinj  6942  caseinl  6944  caseinr  6945  djudom  6946  difinfsn  6953  djuinj  6959  0ct  6960  ctmlemr  6961  ctssdccl  6964  enomnilem  6978  djuassen  7041  xpdjuen  7042  djudoml  7043  djudomr  7044  ltnnnq  7199  nnnq0lem1  7222  addnqprlemfl  7335  addnqprlemfu  7336  mulnqprlemfl  7351  mulnqprlemfu  7352  suplocexprlem2b  7490  prsrlem1  7518  gt0srpr  7524  caucvgsrlemcl  7565  caucvgsrlemfv  7567  caucvgsrlembound  7570  mulcnsr  7611  mulcnsrec  7619  addvalex  7620  pitoregt0  7625  axmulass  7649  axdistr  7650  recriota  7666  mulid1  7731  axmulgt0  7804  cnegexlem2  7906  cnegex  7908  gt0ne0d  8242  recexre  8308  msqge0  8346  mulge0  8349  recgt0  8576  recreclt  8626  cju  8687  nnge1  8711  nnnlt1  8714  nn0nlt0  8971  elz2  9090  nnm1ge0  9105  recnz  9112  zneo  9120  uz3m2nn  9336  eluz2b2  9365  nn01to3  9377  mnflt  9537  xltadd1  9627  lincmb01cmp  9754  iccf1o  9755  fz1n  9792  fseq1p1m1  9842  fznn0  9861  fzctr  9878  4fvwrd4  9885  elfzonlteqm1  9955  divfl0  10037  modqelico  10075  zmodfz  10087  modqid  10090  modqmuladdim  10108  m1modge3gt1  10112  addmodid  10113  frec2uzf1od  10147  frecfzennn  10167  frecfzen2  10168  fzfig  10171  ser0  10255  ser3le  10259  expgt1  10299  expubnd  10318  iexpcyc  10365  binom2sub  10373  binom3  10377  zesq  10378  bernneq  10380  bernneq2  10381  expnbnd  10383  expnlbnd2  10385  facdiv  10452  faclbnd2  10456  faclbnd3  10457  bcval4  10466  hashinfom  10492  hashennn  10494  fihashf1rn  10503  isfinite4im  10507  hashfz  10535  crre  10597  crim  10598  remim  10600  mulreap  10604  cjreb  10606  recj  10607  reneg  10608  readd  10609  remullem  10611  imcj  10615  imneg  10616  imadd  10617  cjadd  10624  cjneg  10630  imval2  10634  cjreim  10643  cnrecnv  10650  uzin2  10727  absval  10741  rennim  10742  resqrexlemcalc3  10756  resqrexlemnm  10758  resqrexlemcvg  10759  resqrexlemgt0  10760  resqrexlemga  10763  absreimsq  10807  absreim  10808  amgm2  10858  climconst2  11028  climshft  11041  climshft2  11043  reccn2ap  11050  climge0  11062  sumsnf  11146  sumnul  11161  isumcl  11162  fsum2dlemstep  11171  fisumcom2  11175  fsumabs  11202  fsumiun  11214  binom  11221  bcxmas  11226  arisum  11235  expcnvap0  11239  explecnv  11242  geosergap  11243  geolim  11248  geolim2  11249  geo2sum  11251  geo2lim  11253  cvgratnnlemrate  11267  cvgratz  11269  mertenslemi1  11272  efcllemp  11291  ege2le3  11304  eftlub  11323  efgt1  11330  tanval2ap  11347  tanval3ap  11348  resinval  11349  recosval  11350  efi4p  11351  resin4p  11352  recos4p  11353  resincl  11354  recoscl  11355  efmival  11367  efeul  11368  sinadd  11370  cosadd  11371  tanaddap  11373  sinmul  11378  cos2tsin  11385  ef01bndlem  11390  sin01bnd  11391  cos01bnd  11392  sin01gt0  11395  cos01gt0  11396  absef  11403  absefib  11404  efieq1re  11405  demoivreALT  11407  eirraplem  11410  odd2np1  11497  oddm1even  11499  oddp1even  11500  oexpneg  11501  opoe  11519  omoe  11520  nn0o1gt2  11529  nn0o  11531  algcvg  11656  algcvgblem  11657  1nprm  11722  1idssfct  11723  oddprmge3  11742  divgcdodd  11748  pw2dvdslemn  11770  pw2dvds  11771  oddpwdclemodd  11777  oddpwdc  11779  phicl2  11817  phibndlem  11819  phibnd  11820  hashdvds  11824  crth  11827  phimullem  11828  hashgcdeq  11831  evenennn  11833  ennnfonelemj0  11841  ennnfonelemjn  11842  ennnfonelemg  11843  ennnfonelemkh  11852  ennnfonelemhf1o  11853  ennnfonelemex  11854  ennnfonelemhom  11855  ennnfonelemnn0  11862  exmidunben  11866  ctinfomlemom  11867  slotex  11913  setscom  11926  setsslid  11936  2strbas1g  11990  2strop1g  11991  rngbaseg  12002  rngplusgg  12003  rngmulrg  12004  srngbased  12009  srngplusgd  12010  srngmulrd  12011  srnginvld  12012  lmodbased  12020  lmodplusgd  12021  lmodscad  12022  lmodvscad  12023  ipsbased  12028  ipsaddgd  12029  ipsmulrd  12030  ipsscad  12031  ipsvscad  12032  ipsipd  12033  topgrpbasd  12038  topgrpplusgd  12039  topgrptsetd  12040  toponsspwpwg  12116  topgele  12123  istps  12126  topontopn  12131  tgvalex  12146  tgclb  12161  lmfval  12288  lmres  12344  ispsmet  12419  psmetge0  12427  ismet  12440  isxmet  12441  xmetge0  12461  isxms2  12548  comet  12595  bdxmet  12597  cnmetdval  12625  cnbl0  12630  cnblcld  12631  reopnap  12634  tgioo  12642  cncfcncntop  12676  cncfmpt2fcntop  12681  limcimolemlt  12729  cnplimcim  12732  cnplimclemr  12734  limccnpcntop  12740  limccnp2lem  12741  limccnp2cntop  12742  dvfvalap  12746  dvbss  12750  dvcnp2cntop  12759  dvcn  12760  dvaddxxbr  12761  dvmulxxbr  12762  dvcoapbr  12767  dvcjbr  12768  dvrecap  12773  dveflem  12782  pilem3  12791  ef2kpi  12814  efper  12815  sinperlem  12816  efimpi  12827  ptolemy  12832  sincosq2sgn  12835  sincosq3sgn  12836  sincosq4sgn  12837  sinq12gt0  12838  cosq14gt0  12840  tangtx  12846  sinkpi  12855  coskpi  12856  cosordlem  12857  pwf1oexmid  13121  isomninnlem  13152
  Copyright terms: Public domain W3C validator