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  392  pm2.13dc  853  hbequid  1476  equidqe  1495  equid  1660  ax10  1678  hbae  1679  vtoclgaf  2723  vtocl2gaf  2725  vtocl3gaf  2727  ifmdc  3477  elinti  3748  copsexg  4134  nlimsucg  4449  tfisi  4469  vtoclr  4555  issref  4889  relresfld  5036  f1o2ndf1  6091  tfrlem9  6182  nndi  6348  mulcanpig  7107  lediv2a  8613  seq3id3  10231  resqrexlemdecn  10735  ndvdssub  11534  nn0seqcvgd  11629  fiinopn  12077  xmetunirn  12433  mopnval  12517  ax1hfs  13073
  Copyright terms: Public domain W3C validator