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

This proof depends on syntax axioms:   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used 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  7227  isacnm  7565  exmidontriimlem3  7585  fsum2d  12227  fprod2d  12415  isstructim  13424  lmodvscl  14750  lgsquad2  16407  clwwlkccat  16847  2alsraln0m  17365