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  1190  3anbi2i  1191  3anbi3i  1192  trubitru  1415  falbifal  1418  eqid  2177  abid2  2298  abid2f  2345  ceqsexg  2867  nnwetri  6917  exmidontriimlem3  7224  fsum2d  11445  fprod2d  11633  isstructim  12478  lmodvscl  13400