ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  simpr GIF 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  442  adantrl  444  adantlll  446  adantlrl  448  adantrll  450  adantrrl  452  simpllr  468  simplrr  470  simprlr  472  simprrr  474  anabs7  489  jcab  516  pm4.38  519  pm5.21  589  ioran  644  pm3.14  645  orabsOLD  702  ordi  704  pm4.39  710  pm5.16  712  intnan  821  intnand  823  bimsc1  853  niabn  857  simp1r  904  simp2r  906  simp3r  908  3anandirs  1205  truan  1223  19.26  1313  19.26OLD  1314  19.40  1444  cbvex  1528  cbvexd  1683  moan  1825  euan  1831
This theorem was proved from axioms:  ax-ia2 98
  Copyright terms: Public domain W3C validator