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  7559  exmidontriimlem3  7579  fsum2d  12202  fprod2d  12390  isstructim  13366  lmodvscl  14641  lgsquad2  16202  clwwlkccat  16642  2alsraln0m  17158