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  129  ibi  176  anidms  397  pm2.13dc  885  hbequid  1513  equidqe  1532  equid  1701  ax10  1717  hbae  1718  vtoclgaf  2804  vtocl2gaf  2806  vtocl3gaf  2808  ifmdc  3576  elinti  3855  copsexg  4246  nlimsucg  4567  tfisi  4588  vtoclr  4676  issref  5013  relresfld  5160  f1o2ndf1  6231  tfrlem9  6322  nndi  6489  mulcanpig  7336  lediv2a  8854  seq3id3  10509  resqrexlemdecn  11023  ndvdssub  11937  nn0seqcvgd  12043  modprm0  12256  fiinopn  13589  xmetunirn  13943  mopnval  14027  ax1hfs  14907
  Copyright terms: Public domain W3C validator