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  1192  3anbi2i  1193  3anbi3i  1194  trubitru  1434  falbifal  1437  eqid  2204  abid2  2325  abid2f  2373  ceqsexg  2900  nnwetri  7012  isacnm  7314  exmidontriimlem3  7334  fsum2d  11688  fprod2d  11876  isstructim  12788  lmodvscl  14009  lgsquad2  15502