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

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

Proof of Theorem simpl
StepHypRef Expression
1 ax-ia1 99 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97
This theorem was proved from axioms:  ax-ia1 99
This theorem is referenced by:  simpli  104  simpld  105  imp  115  adantrd  264  iba  284  pm3.41  314  pm4.45im  317  prth  326  pm4.71  369  adantlr  446  adantrr  448  adantllr  450  adantlrr  452  adantrlr  454  adantrrr  456  simplll  485  simplrl  487  simprll  489  simprrl  491  anabs1  506  jcab  535  pm4.38  537  pm5.21  610  ioran  668  pm3.14  669  pm4.44  695  ordi  728  pm4.39  734  pm5.16  736  pm5.54dc  826  intnanr  838  intnanrd  840  dcan  841  dedlema  875  dedlemb  876  pm4.42r  877  prlem2  880  simp1l  927  simp2l  929  simp3l  931  3anandis  1236  xordc1  1281  anxordi  1288  falantru  1291  19.26  1367  exsimpl  1505  sbequ2  1649  sbcof2  1688  sbequilem  1716  sbequ8  1724  euan  1953  mooran1  1969  eupickbi  1979  2exeu  1989  dimatis  2014  rexim  2407  r19.26  2435  r19.40  2458  rr19.28v  2677  elrab3t  2691  eueq3dc  2709  mosubt  2712  reu6  2724  sbc2iegf  2822  sbcralt  2828  sbcrext  2829  rmob  2844  csbiebt  2880  ssab2  3018  difdif  3063  uneqin  3182  indifdir  3187  undif3ss  3192  rexm  3314  difsn  3492  opprc1  3562  unissel  3600  ssmin  3625  abssexg  3925  opelopabsb  3988  sess1  4059  ordelord  4084  onin  4089  suctr  4124  ordtriexmidlem  4208  tfi  4248  peano1  4260  peano2  4261  0nelxp  4315  0nelelxp  4316  brab2a  4336  mosubopt  4348  posng  4355  opabssxp  4357  ideqg  4430  relssres  4591  trin2  4659  dminss  4681  iota4an  4829  iota2  4836  fun11uni  4912  imadiflem  4921  funimaexg  4926  fneq12  4935  fvelrnb  5164  dffo4  5258  ffnfv  5266  ffvresb  5271  fmptco  5273  fcoconst  5277  fcof1  5366  isotr  5399  isopolem  5404  f1oiso  5408  acexmidlemcase  5450  ovprc1  5483  fnoprabg  5544  op1steq  5747  1stconst  5784  f1o2ndf1  5791  sprmpt2  5798  brtpos2  5807  tpostpos  5820  tposf12  5825  smores  5848  tfrlemi1  5887  freceq1  5919  freceq2  5920  frectfr  5924  omv2  5984  omsuc  5990  nnsucelsuc  6009  nntri3  6014  nnaordi  6017  nnmordi  6025  nnm00  6038  ecexr  6047  ertr  6057  swoer  6070  erth  6086  ecelqsdm  6112  iinerm  6114  ecinxp  6117  erovlem  6134  dom3  6192  dmaddpqlem  6361  distrnqg  6371  ltanqi  6386  ltmnqi  6387  ltaddnq  6390  ltrnqg  6403  ltnnnq  6406  enq0sym  6415  addnq0mo  6430  mulnq0mo  6431  addnnnq0  6432  distrnq0  6442  prarloclemn  6482  prarloc  6486  ltdfpr  6489  genplt2i  6493  addnqprl  6512  addnqpru  6513  nqprl  6533  appdivnq  6544  1idprl  6566  1idpru  6567  ltexpri  6587  recexpr  6610  cauappcvgprlemdisj  6623  addsrmo  6671  mulsrmo  6672  addsrpr  6673  mulsrpr  6674  0idsr  6695  1idsr  6696  archsr  6708  negeu  6999  pncan  7014  pncan3  7016  negsub  7055  posdif  7245  ltnegcon1  7253  subge0  7265  suble0  7266  lesub0  7269  reapval  7360  reapneg  7381  recextlem1  7414  div0ap  7461  recrecap  7467  rec11ap  7468  recgt0  7597  mulgt1  7610  lerec2  7636  recp1lt1  7646  recreclt  7647  ledivp1  7650  nnsub  7733  avglt1  7940  nnrecl  7955  nnnn0addcl  7988  elnn0nn  8000  nn0ge2m1nn  8018  zaddcl  8061  eluzadd  8277  divfnzn  8332  qaddcl  8346  qreccl  8351  cnref1o  8357  ge0p1rp  8389  xrre3  8505  xltnegi  8518  ixxssixx  8541  iccshftr  8632  iccshftl  8634  iccdil  8636  icccntr  8638  elfz2  8651  peano2fzr  8671  fzdcel  8674  fzsplit2  8684  fzaddel  8692  fzrev2  8717  fzrev2i  8718  fzrev3  8719  elfz1b  8722  fseq1p1m1  8726  uzsubfz0  8756  fzosubel3  8822  eluzgtdifelfzo  8823  fzofzp1b  8854  elfzomelpfzo  8857  frec2uzuzd  8869  frec2uzltd  8870  frec2uzrand  8872  expivallem  8910  expival  8911  expinnval  8912  exp1  8915  expcl2lemap  8921  rpexpcl  8928  expnegzap  8943  mulexp  8948  mulexpzap  8949  leexp2r  8962  leexp1a  8963  sq11  8979  subsq  9011  binom2  9015  binom3  9019  zesq  9020  bernneq  9022  crre  9085  cjexp  9121  cjreim2  9132  sqrtsq  9214  sqrtmsq  9215  absid  9225  nn0abscl  9229  bj-indind  9391  bj-omtrans  9416  bj-inf2vnlem1  9430  sscoll2  9448
  Copyright terms: Public domain W3C validator