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  3902  unipw  4017  opeluu  4245  uniexb  4268  unon  4300  onintrab2im  4307  xpexg  4519  resiexg  4723  imaexg  4750  exse2  4770  soirri  4790  djudisj  4821  elxp5  4882  cnvexg  4931  cnviinm  4935  coexg  4938  funssres  5018  f1oabexg  5222  sefvex  5283  ssimaex  5322  mptfvex  5345  f1ompt  5407  fmptcof  5422  resfunexg  5473  mptexg  5477  funfvima3  5483  ovid  5712  ov  5715  ofres  5820  cofunexg  5833  opabex3d  5843  opabex3  5844  oprabexd  5849  1stcof  5885  2ndcof  5886  mpt2exxg  5928  cnvf1o  5941  f2ndf  5942  algrflemg  5946  tposexg  5971  tfrlemisucaccv  6038  tfrlemibxssdm  6040  tfrlemibfn  6041  tfrlemi14d  6046  tfr1onlemsucaccv  6054  tfr1onlembxssdm  6056  tfr1onlembfn  6057  tfr1onlemres  6062  tfrcllemsucaccv  6067  tfrcllembxssdm  6069  tfrcllembfn  6070  tfrcllemres  6075  rdgtfr  6087  rdgruledefgg  6088  rdgon  6099  frecabex  6111  freccllem  6115  frecfcllem  6117  omcl  6170  oeicl  6171  erth  6282  th3qlem1  6340  mapex  6357  pmvalg  6362  mapsnconst  6397  fundmen  6469  cnvct  6472  snfig  6477  unen  6479  xpdom2  6493  mapxpen  6510  phplem2  6515  findcard2  6551  findcard2s  6552  infnfi  6557  relcnvfi  6594  sbthlemi8  6610  sbthlemi10  6612  djur  6694  casef  6716  caseinj  6717  djuinj  6723  djudom  6724  enomnilem  6731  ltnnnq  6919  nnnq0lem1  6942  addnqprlemfl  7055  addnqprlemfu  7056  mulnqprlemfl  7071  mulnqprlemfu  7072  prsrlem1  7225  gt0srpr  7231  caucvgsrlemcl  7271  caucvgsrlemfv  7273  caucvgsrlembound  7276  mulcnsr  7309  mulcnsrec  7317  addvalex  7318  pitoregt0  7323  axmulass  7345  axdistr  7346  recriota  7362  mulid1  7422  axmulgt0  7495  cnegexlem2  7595  cnegex  7597  gt0ne0d  7924  recexre  7989  msqge0  8027  mulge0  8030  recgt0  8239  recreclt  8289  cju  8349  nnge1  8373  nnnlt1  8376  nn0nlt0  8625  elz2  8744  nnm1ge0  8758  recnz  8765  zneo  8773  uz3m2nn  8986  eluz2b2  9015  nn01to3  9027  mnflt  9178  lincmb01cmp  9345  iccf1o  9346  fz1n  9383  fseq1p1m1  9431  fznn0  9450  fzctr  9465  4fvwrd4  9472  elfzonlteqm1  9542  divfl0  9624  modqelico  9662  zmodfz  9674  modqid  9677  modqmuladdim  9695  m1modge3gt1  9699  addmodid  9700  frec2uzf1od  9734  frecfzennn  9754  frecfzen2  9755  fzfig  9758  iser0  9840  serile  9844  expgt1  9884  expubnd  9903  iexpcyc  9949  binom2sub  9957  binom3  9960  zesq  9961  bernneq  9963  bernneq2  9964  expnbnd  9966  expnlbnd2  9968  facdiv  10035  faclbnd2  10039  faclbnd3  10040  bcval4  10049  hashinfom  10075  hashennn  10077  fihashf1rn  10086  isfinite4im  10090  hashfz  10118  crre  10179  crim  10180  remim  10182  mulreap  10186  cjreb  10188  recj  10189  reneg  10190  readd  10191  remullem  10193  imcj  10197  imneg  10198  imadd  10199  cjadd  10206  cjneg  10212  imval2  10216  cjreim  10225  cnrecnv  10232  uzin2  10308  absval  10322  rennim  10323  resqrexlemcalc3  10337  resqrexlemnm  10339  resqrexlemcvg  10340  resqrexlemgt0  10341  resqrexlemga  10344  absreimsq  10388  absreim  10389  amgm2  10439  climconst2  10565  climshft  10578  climshft2  10580  climge0  10598  odd2np1  10740  oddm1even  10742  oddp1even  10743  oexpneg  10744  opoe  10762  omoe  10763  nn0o1gt2  10772  nn0o  10774  ialgcvg  10897  algcvgblem  10898  1nprm  10963  1idssfct  10964  oddprmge3  10983  divgcdodd  10989  pw2dvdslemn  11010  pw2dvds  11011  oddpwdclemodd  11017  oddpwdc  11019  phicl2  11057  phibndlem  11059  phibnd  11060  hashdvds  11064  crth  11067  phimullem  11068  hashgcdeq  11071  evenennn  11073
  Copyright terms: Public domain W3C validator