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

Theorem pm2.43i 47
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  60  impbid  124  ibi  169  anidms  383  pm2.13dc  790  hbequid  1422  equidqe  1441  equid  1605  ax10  1621  hbae  1622  vtoclgaf  2635  vtocl2gaf  2637  vtocl3gaf  2639  elinti  3651  copsexg  4008  nlimsucg  4317  tfisi  4337  vtoclr  4415  issref  4734  relresfld  4874  f1o2ndf1  5876  tfrlem9  5965  nndi  6095  mulcanpig  6490  lediv2a  7935  iseqid3s  9404  resqrexlemdecn  9831  nn0seqcvgd  10235  ax1hfs  10257
  Copyright terms: Public domain W3C validator