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	|- ( ph <-> ph )

Proof of Theorem biid

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ph -> ph )
2	1, 1	impbii 126	1 |- ( ph <-> ph )

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  7229  isacnm  7565  exmidontriimlem3  7585  fsum2d  12226  fprod2d  12414  isstructim  13423  lmodvscl  14749  lgsquad2  16424  clwwlkccat  16864  2alsraln0m  17382