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

Proof of Theorem biid

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

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  1214  3anbi2i  1215  3anbi3i  1216  trubitru  1457  falbifal  1460  eqid  2229  abid2  2350  abid2f  2398  ceqsexg  2932  nnwetri  7101  isacnm  7408  exmidontriimlem3  7428  fsum2d  11986  fprod2d  12174  isstructim  13086  lmodvscl  14309  lgsquad2  15802  clwwlkccat  16196