Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  simpr Structured version   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  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  648  pm3.14  649  orabsOLD  706  ordi  708  pm4.39  714  pm5.16  716  intnan  799  intnand  801  bimsc1  836  niabn  840  simp1r  887  simp2r  889  simp3r  891  3anandirs  1189  truan  1207  19.26  1305  19.26OLD  1306  19.40  1455  cbvexh  1556  cbvexdh  1715  euan  1864  moan  1877  rexex  2233  r19.26  2306  r19.40  2326  cbvraldva2  2398  cbvrexdva2  2399  gencbvex  2460  rspct  2509  rspcimdv  2517  rspcimedv  2518  rr19.28v  2542  reu6  2587 This theorem was proved from axioms:  ax-ia2 98
 Copyright terms: Public domain W3C validator