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

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

Proof of Theorem simpl
StepHypRef Expression
1 ax-ia1 98 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 96
This theorem is referenced by:  simpli  103  simpld  104  imp  114  adantrd  263  iba  283  pm3.41  313  pm4.45im  316  prth  324  pm4.71  368  anidmOLD  375  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  590  ioran  645  pm3.14  646  pm4.44  672  ordi  705  pm4.39  711  pm5.16  713  intnanr  845  intnanrd  847  dedlema  889  dedlemb  890  prlem2  898  simp1l  945  simp2l  947  simp3l  949  3anandis  1246  nic-ax  1289  nic-axALT  1290  19.26  1361  19.26OLD  1362  exsimpl  1497  sbequ2  1613  mooran1  1878  euan  1881  eupickbi  1890  2exeu  1901  2eu2  1905
This theorem was proved from axioms:  ax-ia1 98
  Copyright terms: Public domain W3C validator