ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm2.43i Structured version   Unicode 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  778  hbequid  1403  equidqe  1422  equid  1586  ax10  1602  hbae  1603  vtoclgaf  2612  vtocl2gaf  2614  vtocl3gaf  2616  elinti  3615  copsexg  3972  nlimsucg  4242  tfisi  4253  vtoclr  4331  issref  4650  relresfld  4790  f1o2ndf1  5791  tfrlem9  5876  nndi  6004  mulcanpig  6319  lediv2a  7622  ax1hfs  9213
  Copyright terms: Public domain W3C validator