ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  pm2.43i GIF 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 (𝜑 → (𝜑𝜓))
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-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  2803  vtocl2gaf  2805  vtocl3gaf  2807  ifmdc  3575  elinti  3854  copsexg  4245  nlimsucg  4566  tfisi  4587  vtoclr  4675  issref  5012  relresfld  5159  f1o2ndf1  6229  tfrlem9  6320  nndi  6487  mulcanpig  7334  lediv2a  8852  seq3id3  10507  resqrexlemdecn  11021  ndvdssub  11935  nn0seqcvgd  12041  modprm0  12254  fiinopn  13507  xmetunirn  13861  mopnval  13945  ax1hfs  14824
  Copyright terms: Public domain W3C validator