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

Theorem biid 170
Description: Principle of identity for logical equivalence. Theorem *4.2 of [WhiteheadRussell] p. 117. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
biid (𝜑𝜑)

Proof of Theorem biid
StepHypRef Expression
1 id 19 . 2 (𝜑𝜑)
21, 1impbii 125 1 (𝜑𝜑)
Colors of variables: wff set class
Syntax hints:  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  biidd  171  3anbi1i  1173  3anbi2i  1174  3anbi3i  1175  trubitru  1397  falbifal  1400  eqid  2157  abid2  2278  abid2f  2325  ceqsexg  2840  nnwetri  6860  exmidontriimlem3  7158  fsum2d  11332  fprod2d  11520  isstructim  12215
  Copyright terms: Public domain W3C validator