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

Theorem simpr 103
Description: Elimination of a conjunct. Theorem *3.27 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)
Assertion
Ref Expression
simpr

Proof of Theorem simpr
StepHypRef Expression
1 ax-ia2 100 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97
This theorem was proved from axioms:  ax-ia2 100
This theorem is referenced by:  simpri  106  simprd  107  imp  115  adantld  263  ibar  285  pm3.42  315  pm3.4  316  prth  326  sylancom  397  adantll  445  adantrl  447  adantlll  449  adantlrl  451  adantrll  453  adantrrl  455  simpllr  486  simplrr  488  simprlr  490  simprrr  492  anabs7  508  jcab  535  pm4.38  537  pm5.21  610  ioran  668  pm3.14  669  ordi  728  pm4.39  734  pm5.16  736  pm5.54dc  826  intnan  837  intnand  839  dcan  841  bimsc1  869  niabn  873  simp1r  928  simp2r  930  simp3r  932  3anandirs  1237  truanOLD  1260  bilukdc  1284  19.26  1367  exsimpr  1506  19.40  1519  cbvexh  1635  sbequilem  1716  spsbe  1720  cbvexdh  1798  euan  1953  moan  1966  datisi  2007  fresison  2015  rexex  2362  r19.26  2435  r19.40  2458  cbvraldva2  2531  cbvrexdva2  2532  gencbvex  2594  rspct  2643  rspcimdv  2651  rspcimedv  2652  rr19.28v  2677  elrab3t  2691  reu6  2724  rmob  2844  csbiebt  2880  rabssab  3021  ssddif  3165  difin  3168  difrab  3205  preqsn  3537  opprc2  3563  dfnfc2  3589  intmin4  3634  sndisj  3751  exss  3954  euotd  3982  suctr  4124  tfisi  4253  peano2  4261  relop  4429  releldm  4512  relelrn  4513  resiexg  4596  trin2  4659  xpmlem  4687  unielrel  4788  relcoi2  4791  iota2df  4834  iota2  4836  funopab4  4880  fun11uni  4912  imadiflem  4921  imain  4924  fneq12  4935  f1ssr  5041  fvelrnb  5164  ssimaex  5177  fvmpt2d  5200  fvmptdf  5201  dffo3  5257  ffvresb  5271  fmptco  5273  funfvima3  5335  f1imass  5356  fliftf  5382  fliftval  5383  riota2df  5431  riota5f  5435  acexmidlemcase  5450  ovprc2  5484  eloprabga  5533  eqfnov2  5550  ovmpt2dxf  5568  fnofval  5663  offval2  5668  ofrfval2  5669  caofinvl  5675  2ndrn  5751  1st2ndbr  5752  cnvf1o  5788  f1o2ndf1  5791  mpt2xopoveq  5796  sprmpt2  5798  dftpos4  5819  tpostpos  5820  tposf12  5825  dfsmo2  5843  smores  5848  tfrlem1  5864  tfrlem3ag  5865  tfrlem3a  5866  tfrlemisucaccv  5880  tfrlemi1  5887  tfrexlem  5889  rdgivallem  5908  frecabex  5923  frectfr  5924  frecrdg  5931  freccl  5932  oawordi  5988  nntri3  6014  nnaordi  6017  nnaordex  6036  nnawordex  6037  nnm00  6038  ersymb  6056  ertr  6057  erref  6062  iserd  6068  swoer  6070  erth  6086  iinerm  6114  erinxp  6116  ecinxp  6117  qsel  6119  qliftel  6122  qliftfun  6124  dom3  6192  ssdomg  6194  cnven  6224  dmaddpqlem  6361  nqpi  6362  mulcanenq  6369  ltaddnq  6390  ltexnqq  6391  prarloclemarch2  6402  ltrnqg  6403  ltnnnq  6406  enq0sym  6415  nqnq0pi  6421  nq0nn  6425  mulcanenq0ec  6428  addnq0mo  6430  mulnq0mo  6431  addnnnq0  6432  prloc  6474  prarloclemlt  6476  prarloclemlo  6477  ltdfpr  6489  genplt2i  6493  genpml  6500  genpmu  6501  addnqprllem  6510  addnqprulem  6511  addnqprl  6512  addnqpru  6513  nqprloc  6528  appdivnq  6544  appdiv0nq  6545  mulnqprl  6549  mulnqpru  6550  distrlem1prl  6558  distrlem1pru  6559  ltprordil  6565  1idprl  6566  1idpru  6567  ltexprlemrl  6584  ltexprlemru  6586  ltexpri  6587  addcanprleml  6588  addcanprlemu  6589  recexprlem1ssl  6605  recexpr  6610  aptiprlemu  6612  archpr  6615  cauappcvgprlemopl  6618  cauappcvgprlemdisj  6623  cauappcvgprlemloc  6624  cauappcvgprlemladdfu  6626  cauappcvgprlemladdfl  6627  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  caucvgprlemm  6639  caucvgprlemopl  6640  caucvgprlemloc  6646  caucvgprlemladdfu  6648  caucvgprlemladdrl  6649  caucvgprlemlim  6652  addsrmo  6671  mulsrmo  6672  addsrpr  6673  mulsrpr  6674  0idsr  6695  1idsr  6696  recexsrlem  6702  addgt0sr  6703  axarch  6773  cnegexlem1  6983  cnegex  6986  negeu  6999  pncan  7014  pncan3  7016  npcan  7017  mulneg1  7188  ltnegcon2  7254  add20  7264  subge0  7265  lesub0  7269  reapval  7360  recexre  7362  apreap  7371  ltmul1a  7375  reapneg  7381  cru  7386  apsym  7390  apcotr  7391  apadd1  7392  apneg  7395  mulext1  7396  apti  7406  gt0ap0  7408  recexap  7416  rerecclap  7488  recgt0  7597  prodgt0gt0  7598  lemul1a  7605  lemul12a  7609  lt2msq  7633  ltrec1  7635  recreclt  7647  creui  7693  cju  7694  avglt2  7941  un0addcl  7991  nn0ge2m1nn  8018  nn0nndivcl  8020  elnn0z  8034  peano2z  8057  elz2  8088  peano5uzti  8122  zindd  8132  eluzadd  8277  nn0pzuz  8306  eluz2b2  8316  eqreznegel  8325  nn0ge2m1nnALT  8329  divfnzn  8332  qmulz  8334  qapne  8350  qreccl  8351  cnref1o  8357  ge0p1rp  8389  xrltso  8487  z2ge  8509  xltnegi  8518  ixxssixx  8541  lincmb01cmp  8641  iccf1o  8642  fztri3or  8673  fzdcel  8674  fznlem  8675  fzn  8676  uzsubsubfz  8681  fzsplit2  8684  fzopth  8694  fzdifsuc  8713  fzrev2i  8718  elfz1b  8722  fzneuz  8733  fzrevral  8737  ige2m1fz  8742  elfz0ubfz0  8752  elfz0fzfz0  8753  4fvwrd4  8767  2ffzeq  8768  fzospliti  8802  fzosplit  8803  fzo1fzo0n0  8809  fzonmapblen  8813  fzoaddel  8818  fzosubel  8820  fzosubel3  8822  elfzodifsumelfzo  8827  elfzom1elp1fzo  8828  elfzom1p1elfzo  8840  elfzonelfzo  8856  peano2fzor  8858  frec2uzzd  8867  frec2uzuzd  8869  frec2uzrand  8872  frec2uzf1od  8873  frecuzrdgrrn  8875  frec2uzrdg  8876  frecuzrdgfn  8879  frecuzrdgcl  8880  frecuzrdgsuc  8882  frecfzennn  8884  iseqfeq2  8906  expivallem  8910  expival  8911  expinnval  8912  expp1  8916  rpexpcl  8928  expaddzaplem  8952  leexp1a  8963  exple1  8964  subsq  9011  binom2  9015  binom3  9019  bernneq3  9024  expnbnd  9025  crre  9085  rereb  9091  cjreim2  9132  cjap  9134  sqrt0  9213  nn0abscl  9229  bj-indind  9391  bj-omtrans  9416
  Copyright terms: Public domain W3C validator