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

Theorem sylancr 399
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 397 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105
This theorem is referenced by:  mpteq2da  3873  unipw  3980  opeluu  4209  uniexb  4232  unon  4264  onintrab2im  4271  opeliunxp  4422  xpexg  4479  resiexg  4680  imaexg  4707  exse2  4726  soirri  4746  djudisj  4777  elxp5  4836  cnvexg  4882  cnviinm  4886  coexg  4889  funssres  4969  f1oabexg  5165  sefvex  5223  ssimaex  5261  mptfvex  5283  f1ompt  5347  fmptcof  5358  resfunexg  5409  mptexg  5413  funfvima3  5419  ovid  5644  ov  5647  ofres  5752  cofunexg  5765  opabex3d  5775  opabex3  5776  oprabexd  5781  1stcof  5817  2ndcof  5818  mpt2exxg  5860  cnvf1o  5873  f2ndf  5874  algrflemg  5878  tposexg  5903  tfrlemisucaccv  5969  tfrlemibxssdm  5971  tfrlemibfn  5972  tfrlemi14d  5977  rdgtfr  5991  rdgruledefgg  5992  frecabex  6014  omcl  6071  erth  6180  th3qlem1  6238  fundmen  6316  snfig  6321  unen  6323  xpdom2  6335  phplem2  6346  findcard2  6376  findcard2s  6377  ltnnnq  6578  nnnq0lem1  6601  addnqprlemfl  6714  addnqprlemfu  6715  mulnqprlemfl  6730  mulnqprlemfu  6731  prsrlem1  6884  gt0srpr  6890  caucvgsrlemcl  6930  caucvgsrlemfv  6932  caucvgsrlembound  6935  mulcnsr  6968  mulcnsrec  6976  addvalex  6977  pitoregt0  6982  axmulass  7004  axdistr  7005  recriota  7021  mulid1  7081  axmulgt0  7149  cnegexlem2  7249  cnegex  7251  gt0ne0d  7577  recexre  7642  msqge0  7680  mulge0  7683  recgt0  7890  recreclt  7940  cju  7988  nnge1  8012  nnnlt1  8015  nn0nlt0  8264  elz2  8369  nnm1ge0  8383  recnz  8390  zneo  8397  uz3m2nn  8610  eluz2b2  8636  nn01to3  8648  mnflt  8804  lincmb01cmp  8971  iccf1o  8972  fz1n  9009  fseq1p1m1  9057  fznn0  9075  fzctr  9092  4fvwrd4  9098  elfzonlteqm1  9167  divfl0  9245  modqelico  9283  zmodfz  9295  modqid  9298  modqmuladdim  9316  m1modge3gt1  9320  addmodid  9321  frec2uzf1od  9355  frecuzrdgrom  9359  frecfzennn  9366  frecfzen2  9367  fzfig  9369  iser0  9414  serile  9417  expgt1  9457  expubnd  9476  iexpcyc  9522  binom2sub  9530  binom3  9533  zesq  9534  bernneq  9536  bernneq2  9537  expnbnd  9539  expnlbnd2  9541  facdiv  9605  faclbnd2  9609  faclbnd3  9610  bcval4  9619  crre  9684  crim  9685  remim  9687  mulreap  9691  cjreb  9693  recj  9694  reneg  9695  readd  9696  remullem  9698  imcj  9702  imneg  9703  imadd  9704  cjadd  9711  cjneg  9717  imval2  9721  cjreim  9730  cnrecnv  9737  uzin2  9813  absval  9827  rennim  9828  resqrexlemcalc3  9842  resqrexlemnm  9844  resqrexlemcvg  9845  resqrexlemgt0  9846  resqrexlemga  9849  absreimsq  9893  absreim  9894  amgm2  9944  climconst2  10042  climshft  10055  climshft2  10057  climge0  10075  odd2np1  10183  oddm1even  10185  oddp1even  10186  oexpneg  10187  opoe  10206  omoe  10207  nn0o1gt2  10216  nn0o  10218  pw2dvdslemn  10232  pw2dvds  10233  oddpwdclemodd  10239  oddpwdc  10241  ialgcvg  10249  algcvgblem  10250
  Copyright terms: Public domain W3C validator