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

Theorem pm2.43i 48
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-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  sylc  61  impbid  127  ibi  174  anidms  389  pm2.13dc  813  hbequid  1447  equidqe  1466  equid  1630  ax10  1646  hbae  1647  vtoclgaf  2664  vtocl2gaf  2666  vtocl3gaf  2668  elinti  3653  copsexg  4007  nlimsucg  4317  tfisi  4336  vtoclr  4414  issref  4737  relresfld  4877  f1o2ndf1  5880  tfrlem9  5968  nndi  6130  mulcanpig  6587  lediv2a  8040  iseqid3s  9562  resqrexlemdecn  10036  ndvdssub  10474  nn0seqcvgd  10567  ax1hfs  10944
  Copyright terms: Public domain W3C validator