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  475  3anbi1i  1221  3anbi2i  1222  3anbi3i  1223  trubitru  1464  falbifal  1467  eqid  2238  abid2  2361  abid1  2372  abid2f  2418  ceqsexg  2954  nnwetri  7213  isacnm  7549  exmidontriimlem3  7569  fsum2d  12180  fprod2d  12368  isstructim  13344  lmodvscl  14614  lgsquad2  16116  clwwlkccat  16556