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 )

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  1216  3anbi2i  1217  3anbi3i  1218  trubitru  1459  falbifal  1462  eqid  2230  abid2  2351  abid2f  2399  ceqsexg  2933  nnwetri  7113  isacnm  7423  exmidontriimlem3  7443  fsum2d  12019  fprod2d  12207  isstructim  13119  lmodvscl  14343  lgsquad2  15841  clwwlkccat  16281