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

Theorem sylancr 405
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 403 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106
This theorem is referenced by:  mpteq2da  3901  unipw  4016  opeluu  4244  uniexb  4267  unon  4299  onintrab2im  4306  xpexg  4518  resiexg  4722  imaexg  4749  exse2  4769  soirri  4789  djudisj  4820  elxp5  4881  cnvexg  4930  cnviinm  4934  coexg  4937  funssres  5017  f1oabexg  5221  sefvex  5282  ssimaex  5321  mptfvex  5344  f1ompt  5406  fmptcof  5421  resfunexg  5472  mptexg  5476  funfvima3  5482  ovid  5711  ov  5714  ofres  5819  cofunexg  5832  opabex3d  5842  opabex3  5843  oprabexd  5848  1stcof  5884  2ndcof  5885  mpt2exxg  5927  cnvf1o  5940  f2ndf  5941  algrflemg  5945  tposexg  5970  tfrlemisucaccv  6037  tfrlemibxssdm  6039  tfrlemibfn  6040  tfrlemi14d  6045  tfr1onlemsucaccv  6053  tfr1onlembxssdm  6055  tfr1onlembfn  6056  tfr1onlemres  6061  tfrcllemsucaccv  6066  tfrcllembxssdm  6068  tfrcllembfn  6069  tfrcllemres  6074  rdgtfr  6086  rdgruledefgg  6087  rdgon  6098  frecabex  6110  freccllem  6114  frecfcllem  6116  omcl  6169  oeicl  6170  erth  6281  th3qlem1  6339  mapex  6356  pmvalg  6361  mapsnconst  6396  fundmen  6468  cnvct  6471  snfig  6476  unen  6478  xpdom2  6492  mapxpen  6509  phplem2  6514  findcard2  6550  findcard2s  6551  infnfi  6556  relcnvfi  6593  sbthlemi8  6609  sbthlemi10  6611  djur  6693  casef  6715  caseinj  6716  djuinj  6722  djudom  6723  enomnilem  6730  ltnnnq  6918  nnnq0lem1  6941  addnqprlemfl  7054  addnqprlemfu  7055  mulnqprlemfl  7070  mulnqprlemfu  7071  prsrlem1  7224  gt0srpr  7230  caucvgsrlemcl  7270  caucvgsrlemfv  7272  caucvgsrlembound  7275  mulcnsr  7308  mulcnsrec  7316  addvalex  7317  pitoregt0  7322  axmulass  7344  axdistr  7345  recriota  7361  mulid1  7421  axmulgt0  7494  cnegexlem2  7594  cnegex  7596  gt0ne0d  7923  recexre  7988  msqge0  8026  mulge0  8029  recgt0  8238  recreclt  8288  cju  8348  nnge1  8372  nnnlt1  8375  nn0nlt0  8624  elz2  8743  nnm1ge0  8757  recnz  8764  zneo  8772  uz3m2nn  8985  eluz2b2  9014  nn01to3  9026  mnflt  9177  lincmb01cmp  9344  iccf1o  9345  fz1n  9382  fseq1p1m1  9430  fznn0  9449  fzctr  9464  4fvwrd4  9471  elfzonlteqm1  9541  divfl0  9623  modqelico  9661  zmodfz  9673  modqid  9676  modqmuladdim  9694  m1modge3gt1  9698  addmodid  9699  frec2uzf1od  9733  frecfzennn  9753  frecfzen2  9754  fzfig  9757  iser0  9839  serile  9843  expgt1  9883  expubnd  9902  iexpcyc  9948  binom2sub  9956  binom3  9959  zesq  9960  bernneq  9962  bernneq2  9963  expnbnd  9965  expnlbnd2  9967  facdiv  10034  faclbnd2  10038  faclbnd3  10039  bcval4  10048  hashinfom  10074  hashennn  10076  fihashf1rn  10085  isfinite4im  10089  hashfz  10117  crre  10178  crim  10179  remim  10181  mulreap  10185  cjreb  10187  recj  10188  reneg  10189  readd  10190  remullem  10192  imcj  10196  imneg  10197  imadd  10198  cjadd  10205  cjneg  10211  imval2  10215  cjreim  10224  cnrecnv  10231  uzin2  10307  absval  10321  rennim  10322  resqrexlemcalc3  10336  resqrexlemnm  10338  resqrexlemcvg  10339  resqrexlemgt0  10340  resqrexlemga  10343  absreimsq  10387  absreim  10388  amgm2  10438  climconst2  10564  climshft  10577  climshft2  10579  climge0  10597  odd2np1  10739  oddm1even  10741  oddp1even  10742  oexpneg  10743  opoe  10761  omoe  10762  nn0o1gt2  10771  nn0o  10773  ialgcvg  10896  algcvgblem  10897  1nprm  10962  1idssfct  10963  oddprmge3  10982  divgcdodd  10988  pw2dvdslemn  11009  pw2dvds  11010  oddpwdclemodd  11016  oddpwdc  11018  phicl2  11056  phibndlem  11058  phibnd  11059  hashdvds  11063  crth  11066  phimullem  11067  hashgcdeq  11070  evenennn  11072
  Copyright terms: Public domain W3C validator