ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm2.43i Structured version   GIF version

Theorem pm2.43i 43
Description: Inference absorbing redundant antecedent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.)
Hypothesis
Ref Expression
pm2.43i.1 (φ → (φψ))
Assertion
Ref Expression
pm2.43i (φψ)

Proof of Theorem pm2.43i
StepHypRef Expression
1 id 19 . 2 (φφ)
2 pm2.43i.1 . 2 (φ → (φψ))
31, 2mpd 13 1 (φψ)
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  sylc  56  impbid  120  ibi  165  anidms  377  pm2.13dc  763  hbequid  1382  equidqe  1401  equid  1565  ax10  1581  hbae  1582  vtoclgaf  2589  vtocl2gaf  2591  vtocl3gaf  2593  elinti  3590  copsexg  3947  nlimsucg  4217  tfisi  4228  vtoclr  4306  issref  4625  relresfld  4765  f1o2ndf1  5763  tfrlem9  5848  nndi  5971  mulcanpig  6184  lediv2a  7447  ax1hfs  8355
  Copyright terms: Public domain W3C validator