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  379  pm2.13dc  767  hbequid  1383  equidqe  1402  equidqeOLD  1403  equid  1567  ax10  1583  hbae  1584  vtoclgaf  2591  vtocl2gaf  2593  vtocl3gaf  2595  elinti  3594  copsexg  3951  nlimsucg  4222  tfisi  4233  vtoclr  4311  issref  4630  relresfld  4770  f1o2ndf1  5768  tfrlem9  5853  nndi  5976  mulcanpig  6189  ax1hfs  7144
  Copyright terms: Public domain W3C validator