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

Theorem sylancr 410
Description: Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)
Hypotheses
Ref Expression
sylancr.1 𝜓
sylancr.2 (𝜑𝜒)
sylancr.3 ((𝜓𝜒) → 𝜃)
Assertion
Ref Expression
sylancr (𝜑𝜃)

Proof of Theorem sylancr
StepHypRef Expression
1 sylancr.1 . . 3 𝜓
21a1i 9 . 2 (𝜑𝜓)
3 sylancr.2 . 2 (𝜑𝜒)
4 sylancr.3 . 2 ((𝜓𝜒) → 𝜃)
52, 3, 4syl2anc 408 1 (𝜑𝜃)
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  4017  unipw  4139  opeluu  4371  uniexb  4394  unon  4427  onintrab2im  4434  xpexg  4653  resiexg  4864  imaexg  4893  exse2  4913  soirri  4933  djudisj  4966  elxp5  5027  cnvexg  5076  cnviinm  5080  coexg  5083  funssres  5165  f1oabexg  5379  sefvex  5442  ssimaex  5482  mptfvex  5506  f1ompt  5571  fmptcof  5587  resfunexg  5641  mptexg  5645  funfvima3  5651  ovid  5887  ov  5890  ofres  5996  cofunexg  6009  opabex3d  6019  opabex3  6020  oprabexd  6025  1stcof  6061  2ndcof  6062  mpoexxg  6108  cnvf1o  6122  f2ndf  6123  algrflemg  6127  tposexg  6155  tfrlemisucaccv  6222  tfrlemibxssdm  6224  tfrlemibfn  6225  tfrlemi14d  6230  tfr1onlemsucaccv  6238  tfr1onlembxssdm  6240  tfr1onlembfn  6241  tfr1onlemres  6246  tfrcllemsucaccv  6251  tfrcllembxssdm  6253  tfrcllembfn  6254  tfrcllemres  6259  rdgtfr  6271  rdgruledefgg  6272  rdgon  6283  frecabex  6295  freccllem  6299  frecfcllem  6301  omcl  6357  oeicl  6358  erth  6473  th3qlem1  6531  mapex  6548  pmvalg  6553  mapsnconst  6588  ixpexgg  6616  fundmen  6700  cnvct  6703  snfig  6708  unen  6710  xpdom2  6725  mapxpen  6742  phplem2  6747  findcard2  6783  findcard2s  6784  infnfi  6789  relcnvfi  6829  sbthlemi8  6852  sbthlemi10  6854  fival  6858  fiss  6865  inl11  6950  casef  6973  caseinj  6974  caseinl  6976  caseinr  6977  djudom  6978  difinfsn  6985  djuinj  6991  0ct  6992  ctmlemr  6993  ctssdccl  6996  enomnilem  7010  djuassen  7078  xpdjuen  7079  djudoml  7080  djudomr  7081  cc2lem  7086  ltnnnq  7243  nnnq0lem1  7266  addnqprlemfl  7379  addnqprlemfu  7380  mulnqprlemfl  7395  mulnqprlemfu  7396  suplocexprlem2b  7534  prsrlem1  7562  gt0srpr  7568  caucvgsrlemcl  7609  caucvgsrlemfv  7611  caucvgsrlembound  7614  mulcnsr  7655  mulcnsrec  7663  addvalex  7664  pitoregt0  7669  axmulass  7693  axdistr  7694  recriota  7710  mulid1  7775  axmulgt0  7848  cnegexlem2  7950  cnegex  7952  gt0ne0d  8286  recexre  8352  msqge0  8390  mulge0  8393  recgt0  8620  recreclt  8670  cju  8731  nnge1  8755  nnnlt1  8758  nn0nlt0  9015  elz2  9134  nnm1ge0  9149  recnz  9156  zneo  9164  uz3m2nn  9380  eluz2b2  9409  nn01to3  9421  mnflt  9581  xltadd1  9671  lincmb01cmp  9798  iccf1o  9799  fz1n  9836  fseq1p1m1  9886  fznn0  9905  fzctr  9922  4fvwrd4  9929  elfzonlteqm1  9999  divfl0  10081  modqelico  10119  zmodfz  10131  modqid  10134  modqmuladdim  10152  m1modge3gt1  10156  addmodid  10157  frec2uzf1od  10191  frecfzennn  10211  frecfzen2  10212  fzfig  10215  ser0  10299  ser3le  10303  expgt1  10343  expubnd  10362  iexpcyc  10409  binom2sub  10417  binom3  10421  zesq  10422  bernneq  10424  bernneq2  10425  expnbnd  10427  expnlbnd2  10429  facdiv  10496  faclbnd2  10500  faclbnd3  10501  bcval4  10510  hashinfom  10536  hashennn  10538  fihashf1rn  10547  isfinite4im  10551  hashfz  10579  crre  10641  crim  10642  remim  10644  mulreap  10648  cjreb  10650  recj  10651  reneg  10652  readd  10653  remullem  10655  imcj  10659  imneg  10660  imadd  10661  cjadd  10668  cjneg  10674  imval2  10678  cjreim  10687  cnrecnv  10694  uzin2  10771  absval  10785  rennim  10786  resqrexlemcalc3  10800  resqrexlemnm  10802  resqrexlemcvg  10803  resqrexlemgt0  10804  resqrexlemga  10807  absreimsq  10851  absreim  10852  amgm2  10902  climconst2  11072  climshft  11085  climshft2  11087  reccn2ap  11094  climge0  11106  sumsnf  11190  sumnul  11205  isumcl  11206  fsum2dlemstep  11215  fisumcom2  11219  fsumabs  11246  fsumiun  11258  binom  11265  bcxmas  11270  arisum  11279  expcnvap0  11283  explecnv  11286  geosergap  11287  geolim  11292  geolim2  11293  geo2sum  11295  geo2lim  11297  cvgratnnlemrate  11311  cvgratz  11313  mertenslemi1  11316  prodf1  11323  prodeq2w  11337  efcllemp  11376  ege2le3  11389  eftlub  11408  efgt1  11415  tanval2ap  11431  tanval3ap  11432  resinval  11433  recosval  11434  efi4p  11435  resin4p  11436  recos4p  11437  resincl  11438  recoscl  11439  efmival  11451  efeul  11452  sinadd  11454  cosadd  11455  tanaddap  11457  sinmul  11462  cos2tsin  11469  ef01bndlem  11474  sin01bnd  11475  cos01bnd  11476  sin01gt0  11479  cos01gt0  11480  absef  11487  absefib  11488  efieq1re  11489  demoivreALT  11491  eirraplem  11494  odd2np1  11581  oddm1even  11583  oddp1even  11584  oexpneg  11585  opoe  11603  omoe  11604  nn0o1gt2  11613  nn0o  11615  algcvg  11740  algcvgblem  11741  1nprm  11806  1idssfct  11807  oddprmge3  11826  divgcdodd  11832  pw2dvdslemn  11854  pw2dvds  11855  oddpwdclemodd  11861  oddpwdc  11863  phicl2  11901  phibndlem  11903  phibnd  11904  hashdvds  11908  crth  11911  phimullem  11912  hashgcdeq  11915  evenennn  11917  ennnfonelemj0  11925  ennnfonelemjn  11926  ennnfonelemg  11927  ennnfonelemkh  11936  ennnfonelemhf1o  11937  ennnfonelemex  11938  ennnfonelemhom  11939  ennnfonelemnn0  11946  exmidunben  11950  ctinfomlemom  11951  slotex  12000  setscom  12013  setsslid  12023  2strbas1g  12077  2strop1g  12078  rngbaseg  12089  rngplusgg  12090  rngmulrg  12091  srngbased  12096  srngplusgd  12097  srngmulrd  12098  srnginvld  12099  lmodbased  12107  lmodplusgd  12108  lmodscad  12109  lmodvscad  12110  ipsbased  12115  ipsaddgd  12116  ipsmulrd  12117  ipsscad  12118  ipsvscad  12119  ipsipd  12120  topgrpbasd  12125  topgrpplusgd  12126  topgrptsetd  12127  toponsspwpwg  12203  topgele  12210  istps  12213  topontopn  12218  tgvalex  12233  tgclb  12248  lmfval  12375  lmres  12431  ispsmet  12506  psmetge0  12514  ismet  12527  isxmet  12528  xmetge0  12548  isxms2  12635  comet  12682  bdxmet  12684  cnmetdval  12712  cnbl0  12717  cnblcld  12718  reopnap  12721  tgioo  12729  cncfcncntop  12763  cncfmpt2fcntop  12768  limcimolemlt  12816  cnplimcim  12819  cnplimclemr  12821  limccnpcntop  12827  limccnp2lem  12828  limccnp2cntop  12829  dvfvalap  12833  dvbss  12837  dvcnp2cntop  12846  dvcn  12847  dvaddxxbr  12848  dvmulxxbr  12849  dvcoapbr  12854  dvcjbr  12855  dvrecap  12860  dveflem  12870  reeff1olem  12875  pilem3  12886  ef2kpi  12909  efper  12910  sinperlem  12911  efimpi  12922  ptolemy  12927  sincosq2sgn  12930  sincosq3sgn  12931  sincosq4sgn  12932  sinq12gt0  12933  cosq14gt0  12935  tangtx  12941  sinkpi  12950  coskpi  12951  cosordlem  12952  rplogcl  12977  logge0  12978  logdivlti  12979  pwf1oexmid  13253  isomninnlem  13286
  Copyright terms: Public domain W3C validator