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  3491  opprc1  3561  unissel  3599  ssmin  3624  abssexg  3924  opelopabsb  3987  sess1  4058  ordelord  4083  onin  4088  suctr  4123  ordtriexmidlem  4207  tfi  4247  peano1  4259  peano2  4260  0nelxp  4314  0nelelxp  4315  brab2a  4335  mosubopt  4347  posng  4354  opabssxp  4356  ideqg  4429  relssres  4590  trin2  4658  dminss  4680  iota4an  4828  iota2  4835  fun11uni  4910  imadiflem  4919  funimaexg  4924  fneq12  4933  fvelrnb  5162  dffo4  5256  ffnfv  5264  ffvresb  5269  fmptco  5271  fcoconst  5275  fcof1  5364  isotr  5397  isopolem  5402  f1oiso  5406  acexmidlemcase  5447  ovprc1  5480  fnoprabg  5541  op1steq  5744  1stconst  5781  f1o2ndf1  5788  sprmpt2  5795  brtpos2  5804  tpostpos  5817  tposf12  5822  smores  5845  tfrlemi1  5884  frectfr  5918  omv2  5977  omsuc  5983  nnsucelsuc  6002  nntri3  6007  nnaordi  6010  nnmordi  6018  nnm00  6031  ecexr  6040  ertr  6050  swoer  6063  erth  6079  ecelqsdm  6105  iinerm  6107  ecinxp  6110  erovlem  6127  dom3  6185  dmaddpqlem  6354  distrnqg  6364  ltanqi  6379  ltmnqi  6380  ltaddnq  6383  ltrnqg  6396  enq0sym  6407  addnq0mo  6422  mulnq0mo  6423  addnnnq0  6424  distrnq0  6434  prarloclemn  6474  prarloc  6478  ltdfpr  6481  genplt2i  6485  addnqprl  6505  addnqpru  6506  appdivnq  6534  1idprl  6556  1idpru  6557  ltexpri  6577  recexpr  6600  addsrmo  6623  mulsrmo  6624  addsrpr  6625  mulsrpr  6626  0idsr  6647  1idsr  6648  archsr  6660  negeu  6951  pncan  6966  pncan3  6968  negsub  7007  posdif  7197  ltnegcon1  7205  subge0  7217  suble0  7218  lesub0  7221  reapval  7312  reapneg  7333  recextlem1  7366  div0ap  7413  recrecap  7419  rec11ap  7420  recgt0  7548  mulgt1  7561  lerec2  7587  recp1lt1  7597  recreclt  7598  ledivp1  7601  nnsub  7684  avglt1  7890  nnrecl  7905  nnnn0addcl  7938  elnn0nn  7950  nn0ge2m1nn  7968  zaddcl  8011  eluzadd  8226  divfnzn  8281  qaddcl  8295  qreccl  8300  ge0p1rp  8337  xrre3  8453  xltnegi  8466  ixxssixx  8489  iccshftr  8580  iccshftl  8582  iccdil  8584  icccntr  8586  elfz2  8599  peano2fzr  8619  fzsplit2  8630  fzaddel  8638  fzrev2  8663  fzrev2i  8664  fzrev3  8665  elfz1b  8668  fseq1p1m1  8672  uzsubfz0  8702  fzosubel3  8768  eluzgtdifelfzo  8769  fzofzp1b  8800  elfzomelpfzo  8803  frec2uzuzd  8815  frec2uzltd  8816  frec2uzrand  8818  bj-omtrans  9009  bj-inf2vnlem1  9019  sscoll2  9037
  Copyright terms: Public domain W3C validator