ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm2.43i GIF 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 (𝜑 → (𝜑𝜓))
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  61  impbid  127  ibi  174  anidms  389  pm2.13dc  815  hbequid  1449  equidqe  1468  equid  1632  ax10  1649  hbae  1650  vtoclgaf  2677  vtocl2gaf  2679  vtocl3gaf  2681  ifmdc  3414  elinti  3680  copsexg  4045  nlimsucg  4355  tfisi  4375  vtoclr  4454  issref  4781  relresfld  4926  f1o2ndf1  5950  tfrlem9  6038  nndi  6201  mulcanpig  6838  lediv2a  8291  iseqid3s  9841  resqrexlemdecn  10340  ndvdssub  10805  nn0seqcvgd  10898  ax1hfs  11354
  Copyright terms: Public domain W3C validator