ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm2.43i 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  |-  ( 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  56  impbid  120  ibi  165  anidms  377  pm2.13dc  779  hbequid  1406  equidqe  1425  equid  1589  ax10  1605  hbae  1606  vtoclgaf  2618  vtocl2gaf  2620  vtocl3gaf  2622  elinti  3624  copsexg  3981  nlimsucg  4290  tfisi  4310  vtoclr  4388  issref  4707  relresfld  4847  f1o2ndf1  5849  tfrlem9  5935  nndi  6065  mulcanpig  6433  lediv2a  7861  iseqid3s  9246  resqrexlemdecn  9610  nn0seqcvgd  9880  ax1hfs  9898
  Copyright terms: Public domain W3C validator