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  813  hbequid  1447  equidqe  1466  equid  1630  ax10  1647  hbae  1648  vtoclgaf  2672  vtocl2gaf  2674  vtocl3gaf  2676  elinti  3665  copsexg  4027  nlimsucg  4337  tfisi  4356  vtoclr  4434  issref  4757  relresfld  4897  f1o2ndf1  5901  tfrlem9  5989  nndi  6151  mulcanpig  6657  lediv2a  8110  iseqid3s  9632  resqrexlemdecn  10117  ndvdssub  10555  nn0seqcvgd  10648  ax1hfs  11071
  Copyright terms: Public domain W3C validator