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-1 5  ax-2 6  ax-3 7  ax-mp 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