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

Theorem simpr 101
Description: Elimination of a conjunct. Theorem *3.27 (Simp) of [WhiteheadRussell] p. 112. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 13-Nov-2012.)
Assertion
Ref Expression
simpr

Proof of Theorem simpr
StepHypRef Expression
1 ax-ia2 98 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 95
This theorem is referenced by:  simpri  104  simprd  105  imp  113  adantld  261  ibar  283  pm3.42  313  pm3.4  314  prth  323  sylancom  395  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  592  ioran  647  pm3.14  648  orabsOLD  705  ordi  707  pm4.39  713  pm5.16  715  intnan  795  intnand  797  bimsc1  832  niabn  836  simp1r  883  simp2r  885  simp3r  887  3anandirs  1184  truan  1202  19.26  1300  19.26OLD  1301  19.40  1436  cbvexh  1522  cbvexd  1681  moan  2121  euan  2127
This theorem was proved from axioms:  ax-ia2 98
  Copyright terms: Public domain W3C validator