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

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (φ → φ)
2	1, 1	impbii 180	1 ⊢ (φ ↔ φ)

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  2471  abid2f  2515  ceqsexg  2971  opksnelsik  4266  restxp  5787  oqelins4  5795