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

Theorem biid 171
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 126 1  |-  ( ph  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  biidd  172  an21  471  3anbi1i  1192  3anbi2i  1193  3anbi3i  1194  trubitru  1426  falbifal  1429  eqid  2193  abid2  2314  abid2f  2362  ceqsexg  2888  nnwetri  6963  exmidontriimlem3  7273  fsum2d  11565  fprod2d  11753  isstructim  12619  lmodvscl  13779
  Copyright terms: Public domain W3C validator