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  1217  3anbi2i  1218  3anbi3i  1219  trubitru  1460  falbifal  1463  eqid  2232  abid2  2355  abid1  2366  abid2f  2410  ceqsexg  2945  nnwetri  7176  isacnm  7510  exmidontriimlem3  7530  fsum2d  12121  fprod2d  12309  isstructim  13226  lmodvscl  14453  lgsquad2  15956  clwwlkccat  16396