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

Theorem simpr 102
Description: Elimination of a conjunct. Theorem *3.27 (Simp) of [WhiteheadRussell] p. 112. (The proof was shortened by Wolf Lammen, 13-Nov-2012.)
Assertion
Ref Expression
simpr

Proof of Theorem simpr
StepHypRef Expression
1 ax-ia2 99 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 96
This theorem is referenced by:  simpri  105  simprd  106  imp  114  adantld  262  ibar  284  pm3.42  314  pm3.4  315  prth  324  sylancom  397  adantll  443  adantrl  445  adantlll  447  adantlrl  449  adantrll  451  adantrrl  453  simpllr  469  simplrr  471  simprlr  473  simprrr  475  anabs7  490  jcab  517  pm4.38  520  pm5.21  590  ioran  645  pm3.14  646  orabsOLD  703  ordi  705  pm4.39  711  pm5.16  713  intnan  844  intnand  846  bimsc1  873  niabn  886  dedlem0b  888  simp1r  946  simp2r  948  simp3r  950  3anandirs  1247  19.26  1361  19.26OLD  1362  19.40  1522  cbvex  1600  moan  1875  euan  1881
This theorem was proved from axioms:  ax-ia2 99
  Copyright terms: Public domain W3C validator