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

Theorem sylancr 405
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 403 1 (𝜑𝜃)
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  3869  unipw  3974  opeluu  4202  uniexb  4225  unon  4257  onintrab2im  4264  xpexg  4474  resiexg  4677  imaexg  4704  exse2  4723  soirri  4743  djudisj  4774  elxp5  4833  cnvexg  4879  cnviinm  4883  coexg  4886  funssres  4966  f1oabexg  5163  sefvex  5221  ssimaex  5260  mptfvex  5282  f1ompt  5346  fmptcof  5357  resfunexg  5408  mptexg  5412  funfvima3  5418  ovid  5642  ov  5645  ofres  5750  cofunexg  5763  opabex3d  5773  opabex3  5774  oprabexd  5779  1stcof  5815  2ndcof  5816  mpt2exxg  5858  cnvf1o  5871  f2ndf  5872  algrflemg  5876  tposexg  5901  tfrlemisucaccv  5968  tfrlemibxssdm  5970  tfrlemibfn  5971  tfrlemi14d  5976  tfr1onlemsucaccv  5984  tfr1onlembxssdm  5986  tfr1onlembfn  5987  tfr1onlemres  5992  tfrcllemsucaccv  5997  tfrcllembxssdm  5999  tfrcllembfn  6000  tfrcllemres  6005  rdgtfr  6017  rdgruledefgg  6018  rdgon  6029  frecabex  6041  freccllem  6045  frecfcllem  6047  omcl  6099  oeicl  6100  erth  6209  th3qlem1  6267  fundmen  6345  snfig  6350  unen  6352  xpdom2  6365  phplem2  6378  findcard2  6413  findcard2s  6414  infnfi  6419  relcnvfi  6439  ltnnnq  6664  nnnq0lem1  6687  addnqprlemfl  6800  addnqprlemfu  6801  mulnqprlemfl  6816  mulnqprlemfu  6817  prsrlem1  6970  gt0srpr  6976  caucvgsrlemcl  7016  caucvgsrlemfv  7018  caucvgsrlembound  7021  mulcnsr  7054  mulcnsrec  7062  addvalex  7063  pitoregt0  7068  axmulass  7090  axdistr  7091  recriota  7107  mulid1  7167  axmulgt0  7240  cnegexlem2  7340  cnegex  7342  gt0ne0d  7669  recexre  7734  msqge0  7772  mulge0  7775  recgt0  7984  recreclt  8034  cju  8094  nnge1  8118  nnnlt1  8121  nn0nlt0  8370  elz2  8489  nnm1ge0  8503  recnz  8510  zneo  8518  uz3m2nn  8731  eluz2b2  8760  nn01to3  8772  mnflt  8923  lincmb01cmp  9090  iccf1o  9091  fz1n  9128  fseq1p1m1  9176  fznn0  9195  fzctr  9210  4fvwrd4  9216  elfzonlteqm1  9285  divfl0  9367  modqelico  9405  zmodfz  9417  modqid  9420  modqmuladdim  9438  m1modge3gt1  9442  addmodid  9443  frec2uzf1od  9477  frecfzennn  9497  frecfzen2  9498  fzfig  9501  iser0  9557  serile  9560  expgt1  9600  expubnd  9619  iexpcyc  9665  binom2sub  9673  binom3  9676  zesq  9677  bernneq  9679  bernneq2  9680  expnbnd  9682  expnlbnd2  9684  facdiv  9751  faclbnd2  9755  faclbnd3  9756  bcval4  9765  sizeinf  9791  sizeennn  9793  sizef1rn  9802  isfinite4im  9806  crre  9871  crim  9872  remim  9874  mulreap  9878  cjreb  9880  recj  9881  reneg  9882  readd  9883  remullem  9885  imcj  9889  imneg  9890  imadd  9891  cjadd  9898  cjneg  9904  imval2  9908  cjreim  9917  cnrecnv  9924  uzin2  10000  absval  10014  rennim  10015  resqrexlemcalc3  10029  resqrexlemnm  10031  resqrexlemcvg  10032  resqrexlemgt0  10033  resqrexlemga  10036  absreimsq  10080  absreim  10081  amgm2  10131  climconst2  10257  climshft  10270  climshft2  10272  climge0  10290  odd2np1  10406  oddm1even  10408  oddp1even  10409  oexpneg  10410  opoe  10428  omoe  10429  nn0o1gt2  10438  nn0o  10440  ialgcvg  10563  algcvgblem  10564  1nprm  10629  1idssfct  10630  oddprmge3  10649  divgcdodd  10655  pw2dvdslemn  10676  pw2dvds  10677  oddpwdclemodd  10683  oddpwdc  10685
  Copyright terms: Public domain W3C validator