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  3887  unipw  4000  opeluu  4228  uniexb  4251  unon  4283  onintrab2im  4290  xpexg  4500  resiexg  4703  imaexg  4730  exse2  4749  soirri  4769  djudisj  4800  elxp5  4859  cnvexg  4905  cnviinm  4909  coexg  4912  funssres  4992  f1oabexg  5190  sefvex  5248  ssimaex  5287  mptfvex  5309  f1ompt  5373  fmptcof  5384  resfunexg  5435  mptexg  5439  funfvima3  5445  ovid  5669  ov  5672  ofres  5777  cofunexg  5790  opabex3d  5800  opabex3  5801  oprabexd  5806  1stcof  5842  2ndcof  5843  mpt2exxg  5885  cnvf1o  5898  f2ndf  5899  algrflemg  5903  tposexg  5928  tfrlemisucaccv  5995  tfrlemibxssdm  5997  tfrlemibfn  5998  tfrlemi14d  6003  tfr1onlemsucaccv  6011  tfr1onlembxssdm  6013  tfr1onlembfn  6014  tfr1onlemres  6019  tfrcllemsucaccv  6024  tfrcllembxssdm  6026  tfrcllembfn  6027  tfrcllemres  6032  rdgtfr  6044  rdgruledefgg  6045  rdgon  6056  frecabex  6068  freccllem  6072  frecfcllem  6074  omcl  6126  oeicl  6127  erth  6238  th3qlem1  6296  fundmen  6375  cnvct  6378  snfig  6381  unen  6383  xpdom2  6397  phplem2  6410  findcard2  6446  findcard2s  6447  infnfi  6452  relcnvfi  6482  djur  6563  ltnnnq  6745  nnnq0lem1  6768  addnqprlemfl  6881  addnqprlemfu  6882  mulnqprlemfl  6897  mulnqprlemfu  6898  prsrlem1  7051  gt0srpr  7057  caucvgsrlemcl  7097  caucvgsrlemfv  7099  caucvgsrlembound  7102  mulcnsr  7135  mulcnsrec  7143  addvalex  7144  pitoregt0  7149  axmulass  7171  axdistr  7172  recriota  7188  mulid1  7248  axmulgt0  7321  cnegexlem2  7421  cnegex  7423  gt0ne0d  7750  recexre  7815  msqge0  7853  mulge0  7856  recgt0  8065  recreclt  8115  cju  8175  nnge1  8199  nnnlt1  8202  nn0nlt0  8451  elz2  8570  nnm1ge0  8584  recnz  8591  zneo  8599  uz3m2nn  8812  eluz2b2  8841  nn01to3  8853  mnflt  9004  lincmb01cmp  9171  iccf1o  9172  fz1n  9209  fseq1p1m1  9257  fznn0  9276  fzctr  9291  4fvwrd4  9297  elfzonlteqm1  9366  divfl0  9448  modqelico  9486  zmodfz  9498  modqid  9501  modqmuladdim  9519  m1modge3gt1  9523  addmodid  9524  frec2uzf1od  9558  frecfzennn  9578  frecfzen2  9579  fzfig  9582  iser0  9638  serile  9641  expgt1  9681  expubnd  9700  iexpcyc  9746  binom2sub  9754  binom3  9757  zesq  9758  bernneq  9760  bernneq2  9761  expnbnd  9763  expnlbnd2  9765  facdiv  9832  faclbnd2  9836  faclbnd3  9837  bcval4  9846  hashinfom  9872  hashennn  9874  fihashf1rn  9883  isfinite4im  9887  hashfz  9915  crre  9963  crim  9964  remim  9966  mulreap  9970  cjreb  9972  recj  9973  reneg  9974  readd  9975  remullem  9977  imcj  9981  imneg  9982  imadd  9983  cjadd  9990  cjneg  9996  imval2  10000  cjreim  10009  cnrecnv  10016  uzin2  10092  absval  10106  rennim  10107  resqrexlemcalc3  10121  resqrexlemnm  10123  resqrexlemcvg  10124  resqrexlemgt0  10125  resqrexlemga  10128  absreimsq  10172  absreim  10173  amgm2  10223  climconst2  10349  climshft  10362  climshft2  10364  climge0  10382  odd2np1  10498  oddm1even  10500  oddp1even  10501  oexpneg  10502  opoe  10520  omoe  10521  nn0o1gt2  10530  nn0o  10532  ialgcvg  10655  algcvgblem  10656  1nprm  10721  1idssfct  10722  oddprmge3  10741  divgcdodd  10747  pw2dvdslemn  10768  pw2dvds  10769  oddpwdclemodd  10775  oddpwdc  10777  phicl2  10815  phibndlem  10817  phibnd  10818  hashdvds  10822  crth  10825  phimullem  10826  hashgcdeq  10829  evenennn  10831
  Copyright terms: Public domain W3C validator