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

Theorem simpl 100
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 97 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 95
This theorem is referenced by:  simpli  102  simpld  103  imp  113  adantrd  262  iba  282  pm3.41  312  pm4.45im  315  prth  323  pm4.71  366  anidmOLD  373  adantlr  444  adantrr  446  adantllr  448  adantlrr  450  adantrlr  452  adantrrr  454  simplll  468  simplrl  470  simprll  472  simprrl  474  anabs1  488  jcab  517  pm4.38  520  pm5.21  592  ioran  647  pm3.14  648  pm4.44  674  ordi  707  pm4.39  713  pm5.16  715  intnanr  796  intnanrd  798  prlem2  839  simp1l  882  simp2l  884  simp3l  886  3anandis  1183  19.26  1300  19.26OLD  1301  exsimpl  1425  sbequ2  1539  mooran1  2124  euan  2127  eupickbi  2136  2exeu  2147  2eu2  2151
This theorem was proved from axioms:  ax-ia1 97
  Copyright terms: Public domain W3C validator