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  anidmOLD  377  adantlr  449  adantrr  451  adantllr  453  adantlrr  455  adantrlr  457  adantrrr  459  simplll  473  simplrl  475  simprll  477  simprrl  479  anabs1  493  jcab  522  pm4.38  525  pm5.21  598  ioran  656  pm3.14  657  pm4.44  683  ordi  717  pm4.39  723  pm5.16  725  intnanr  827  intnanrd  829  dedlema  864  dedlemb  865  prlem2  869  simp1l  916  simp2l  918  simp3l  920  3anandis  1222  anxordi  1274  19.26  1350  exsimpl  1490  sbequ2  1634  euan  1938  mooran1  1954  eupickbi  1964  2exeu  1974  dimatis  1999  r19.26  2419  r19.40  2442  rr19.28v  2660  elrab3t  2674  eueq3dc  2692  reu6  2707  sbc2iegf  2805  sbcralt  2811  sbcrext  2812  rmob  2827  csbiebt  2863  ssab2  3001  uneqin  3165  undif3ss  3175  difsn  3475  opprc1  3545  unissel  3583  ssmin  3608  abssexg  3908  sess1  4042  onin  4072  suctrALT  4107  0nelxp  4299  0nelelxp  4300  brab2a  4320  posng  4339  opabssxp  4341  ideqg  4414  relssres  4575  trin2  4643  dminss  4665  iota4an  4813  iota2  4820  fun11uni  4895  fneq12  4918  dffo4  5240  ffnfv  5248  ffvresb  5253  fmptco  5255  fcoconst  5259  fcof1  5348  isotr  5381  isopolem  5386  f1oiso  5390  ovprc1  5464  fnoprabg  5525  op1steq  5728  1stconst  5765  f1o2ndf1  5772  sprmpt2  5779  tpostpos  5801  tposf12  5806  smores  5829  tfrlemi1  5867  tfrlemi14  5869  nnmordi  6000  ertr  6032  swoer  6045  erth  6061  ecelqsdm  6087  iinerm  6089  ecinxp  6092  erovlem  6109  distrnqg  6246  ltanqi  6261  ltmnqi  6262  distrnq0  6314  addnqprl  6384  addnqpru  6385  appdivnq  6407  1idprl  6429  1idpru  6430  ltexpri  6450  recexpr  6472  addsrmo  6490  mulsrmo  6491  addsrpr  6492  mulsrpr  6493  0idsr  6514  1idsr  6515  negeu  6789  pncan  6804  pncan3  6806  negsub  6845  sscoll2  7206
  Copyright terms: Public domain W3C validator