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  880  hbequid  1506  equidqe  1525  equid  1694  ax10  1710  hbae  1711  vtoclgaf  2795  vtocl2gaf  2797  vtocl3gaf  2799  ifmdc  3565  elinti  3840  copsexg  4229  nlimsucg  4550  tfisi  4571  vtoclr  4659  issref  4993  relresfld  5140  f1o2ndf1  6207  tfrlem9  6298  nndi  6465  mulcanpig  7297  lediv2a  8811  seq3id3  10463  resqrexlemdecn  10976  ndvdssub  11889  nn0seqcvgd  11995  modprm0  12208  fiinopn  12796  xmetunirn  13152  mopnval  13236  ax1hfs  14103
  Copyright terms: Public domain W3C validator