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  1193  3anbi2i  1194  3anbi3i  1195  trubitru  1435  falbifal  1438  eqid  2207  abid2  2328  abid2f  2376  ceqsexg  2908  nnwetri  7039  isacnm  7346  exmidontriimlem3  7366  fsum2d  11861  fprod2d  12049  isstructim  12961  lmodvscl  14182  lgsquad2  15675