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  enq0sym  6414  addnq0mo  6429  mulnq0mo  6430  addnnnq0  6431  distrnq0  6441  prarloclemn  6481  prarloc  6485  ltdfpr  6488  genplt2i  6492  addnqprl  6511  addnqpru  6512  nqprl  6532  appdivnq  6543  1idprl  6565  1idpru  6566  ltexpri  6586  recexpr  6609  cauappcvgprlemdisj  6622  addsrmo  6651  mulsrmo  6652  addsrpr  6653  mulsrpr  6654  0idsr  6675  1idsr  6676  archsr  6688  negeu  6979  pncan  6994  pncan3  6996  negsub  7035  posdif  7225  ltnegcon1  7233  subge0  7245  suble0  7246  lesub0  7249  reapval  7340  reapneg  7361  recextlem1  7394  div0ap  7441  recrecap  7447  rec11ap  7448  recgt0  7577  mulgt1  7590  lerec2  7616  recp1lt1  7626  recreclt  7627  ledivp1  7630  nnsub  7713  avglt1  7920  nnrecl  7935  nnnn0addcl  7968  elnn0nn  7980  nn0ge2m1nn  7998  zaddcl  8041  eluzadd  8257  divfnzn  8312  qaddcl  8326  qreccl  8331  cnref1o  8337  ge0p1rp  8369  xrre3  8485  xltnegi  8498  ixxssixx  8521  iccshftr  8612  iccshftl  8614  iccdil  8616  icccntr  8618  elfz2  8631  peano2fzr  8651  fzdcel  8654  fzsplit2  8664  fzaddel  8672  fzrev2  8697  fzrev2i  8698  fzrev3  8699  elfz1b  8702  fseq1p1m1  8706  uzsubfz0  8736  fzosubel3  8802  eluzgtdifelfzo  8803  fzofzp1b  8834  elfzomelpfzo  8837  frec2uzuzd  8849  frec2uzltd  8850  frec2uzrand  8852  expivallem  8890  expival  8891  expinnval  8892  exp1  8895  expcl2lemap  8901  rpexpcl  8908  expnegzap  8923  mulexp  8928  mulexpzap  8929  leexp2r  8942  leexp1a  8943  sq11  8959  subsq  8991  binom2  8995  binom3  8999  zesq  9000  bernneq  9002  crre  9065  cjexp  9101  cjreim2  9112  sqrtsq  9194  sqrtmsq  9195  absid  9205  nn0abscl  9209  bj-omtrans  9390  bj-inf2vnlem1  9400  sscoll2  9418
  Copyright terms: Public domain W3C validator