ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  simpl Structured version   GIF 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  6512  addnqpru  6513  appdivnq  6542  1idprl  6564  1idpru  6565  ltexpri  6585  recexpr  6608  addsrmo  6631  mulsrmo  6632  addsrpr  6633  mulsrpr  6634  0idsr  6655  1idsr  6656  archsr  6668  negeu  6959  pncan  6974  pncan3  6976  negsub  7015  posdif  7205  ltnegcon1  7213  subge0  7225  suble0  7226  lesub0  7229  reapval  7320  reapneg  7341  recextlem1  7374  div0ap  7421  recrecap  7427  rec11ap  7428  recgt0  7557  mulgt1  7570  lerec2  7596  recp1lt1  7606  recreclt  7607  ledivp1  7610  nnsub  7693  avglt1  7900  nnrecl  7915  nnnn0addcl  7948  elnn0nn  7960  nn0ge2m1nn  7978  zaddcl  8021  eluzadd  8237  divfnzn  8292  qaddcl  8306  qreccl  8311  cnref1o  8317  ge0p1rp  8349  xrre3  8465  xltnegi  8478  ixxssixx  8501  iccshftr  8592  iccshftl  8594  iccdil  8596  icccntr  8598  elfz2  8611  peano2fzr  8631  fzdcel  8634  fzsplit2  8644  fzaddel  8652  fzrev2  8677  fzrev2i  8678  fzrev3  8679  elfz1b  8682  fseq1p1m1  8686  uzsubfz0  8716  fzosubel3  8782  eluzgtdifelfzo  8783  fzofzp1b  8814  elfzomelpfzo  8817  frec2uzuzd  8829  frec2uzltd  8830  frec2uzrand  8832  expivallem  8870  expival  8871  expinnval  8872  exp1  8875  expcl2lemap  8881  rpexpcl  8888  expnegzap  8903  mulexp  8908  mulexpzap  8909  leexp2r  8922  leexp1a  8923  sq11  8939  subsq  8971  binom2  8975  binom3  8979  zesq  8980  bernneq  8982  crre  9045  cjexp  9081  cjreim2  9092  bj-omtrans  9344  bj-inf2vnlem1  9354  sscoll2  9372
  Copyright terms: Public domain W3C validator