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

Theorem pm2.43i 49
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  |-  ( ph  ->  ( ph  ->  ps ) )
Assertion
Ref Expression
pm2.43i  |-  ( ph  ->  ps )

Proof of Theorem pm2.43i
StepHypRef Expression
1 id 19 . 2  |-  ( ph  ->  ph )
2 pm2.43i.1 . 2  |-  ( ph  ->  ( ph  ->  ps ) )
31, 2mpd 13 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  sylc  62  impbid  128  ibi  175  anidms  394  pm2.13dc  855  hbequid  1478  equidqe  1497  equid  1662  ax10  1680  hbae  1681  vtoclgaf  2725  vtocl2gaf  2727  vtocl3gaf  2729  ifmdc  3479  elinti  3750  copsexg  4136  nlimsucg  4451  tfisi  4471  vtoclr  4557  issref  4891  relresfld  5038  f1o2ndf1  6093  tfrlem9  6184  nndi  6350  mulcanpig  7111  lediv2a  8621  seq3id3  10248  resqrexlemdecn  10752  ndvdssub  11554  nn0seqcvgd  11649  fiinopn  12098  xmetunirn  12454  mopnval  12538  ax1hfs  13167
  Copyright terms: Public domain W3C validator