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  2802  vtocl2gaf  2804  vtocl3gaf  2806  ifmdc  3574  elinti  3853  copsexg  4244  nlimsucg  4565  tfisi  4586  vtoclr  4674  issref  5011  relresfld  5158  f1o2ndf1  6228  tfrlem9  6319  nndi  6486  mulcanpig  7333  lediv2a  8851  seq3id3  10506  resqrexlemdecn  11020  ndvdssub  11934  nn0seqcvgd  12040  modprm0  12253  fiinopn  13474  xmetunirn  13828  mopnval  13912  ax1hfs  14791
  Copyright terms: Public domain W3C validator