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  7223  isacnm  7560  exmidontriimlem3  7580  fsum2d  12221  fprod2d  12409  isstructim  13418  lmodvscl  14725  lgsquad2  16368  clwwlkccat  16808  2alsraln0m  17325