NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  biid Unicode version

Theorem biid 227
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 180 1
Colors of variables: wff setvar class
Syntax hints:   wb 176
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 177
This theorem is referenced by:  biidd  228  pm5.19  349  3anbi1i  1142  3anbi2i  1143  3anbi3i  1144  trujust  1318  tru  1321  trubitru  1350  falbifal  1353  hadcoma  1388  hadcomb  1389  hadnot  1393  cadcomb  1396  eqid  2353  abid2  2470  abid2f  2514  ceqsexg  2970  opksnelsik  4265  restxp  5786  oqelins4  5794
  Copyright terms: Public domain W3C validator