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  128  ibi  175  anidms  395  pm2.13dc  871  hbequid  1493  equidqe  1512  equid  1681  ax10  1697  hbae  1698  vtoclgaf  2777  vtocl2gaf  2779  vtocl3gaf  2781  ifmdc  3543  elinti  3818  copsexg  4206  nlimsucg  4527  tfisi  4548  vtoclr  4636  issref  4970  relresfld  5117  f1o2ndf1  6177  tfrlem9  6268  nndi  6435  mulcanpig  7257  lediv2a  8771  seq3id3  10415  resqrexlemdecn  10923  ndvdssub  11833  nn0seqcvgd  11933  modprm0  12144  fiinopn  12472  xmetunirn  12828  mopnval  12912  ax1hfs  13713
  Copyright terms: Public domain W3C validator