ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  biid Unicode 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  |-  ( ph  <->  ph )

Proof of Theorem biid
StepHypRef Expression
1 id 19 . 2  |-  ( ph  ->  ph )
21, 1impbii 125 1  |-  ( ph  <->  ph )
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  1179  3anbi2i  1180  3anbi3i  1181  trubitru  1404  falbifal  1407  eqid  2164  abid2  2285  abid2f  2332  ceqsexg  2850  nnwetri  6873  exmidontriimlem3  7171  fsum2d  11363  fprod2d  11551  isstructim  12362
  Copyright terms: Public domain W3C validator