ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  idd GIF version

Theorem idd 21
Description: Principle of identity with antecedent. (Contributed by NM, 26-Nov-1995.)
Assertion
Ref Expression
idd (𝜑 → (𝜓𝜓))

Proof of Theorem idd
StepHypRef Expression
1 id 19 . 2 (𝜓𝜓)
21a1i 9 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:  imim1d  75  ancld  321  ancrd  322  anim12d  331  anim1d  332  anim2d  333  orel2  698  pm2.621  719  orim1d  759  orim2d  760  pm2.63  772  pm2.74  779  simprimdc  827  oplem1  942  equsex  1689  equsexd  1690  r19.36av  2557  r19.44av  2565  r19.45av  2566  reuss  3325  opthpr  3667  relop  4657  swoord2  6425  indpi  7114  lelttr  7816  elnnz  9018  ztri3or0  9050  xrlelttr  9540  icossicc  9694  iocssicc  9695  ioossico  9696  lmconst  12291  cnptopresti  12313  sslm  12322  bj-exlimmp  12810
  Copyright terms: Public domain W3C validator