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	⊢ (𝜑 ↔ 𝜑)

Proof of Theorem biid

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

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  an21  468  3anbi1i  1185  3anbi2i  1186  3anbi3i  1187  trubitru  1410  falbifal  1413  eqid  2170  abid2  2291  abid2f  2338  ceqsexg  2858  nnwetri  6893  exmidontriimlem3  7200  fsum2d  11398  fprod2d  11586  isstructim  12430