Theorem pm4.2 170

Description: Principle of identity for logical equivalence. Theorem *4.2 of [WhiteheadRussell] p. 117.

Assertion

Ref	Expression
pm4.2	|- (ph <-> ph)

Proof of Theorem pm4.2

Step	Hyp	Ref	Expression
1		id 59	. 2 |- (ph -> ph)
2	1, 1	impbi 157	1 |- (ph <-> ph)

Syntax hints:   <-> wb 146

This theorem is referenced by:  pm4.2d 171  pm5.19 671  3anbi1i 826  3anbi2i 827  3anbi3i 828  eqid 1478  abid2 1583  ralbii 1670  rexbii 1671  ceqsexg 1890  wecmpep 2947  ordon 2993  aceq5 4750  aceqkm 4791  zorn 4807  elfz2nn0t 6496  climadd 7117  climmul 7128  climcmp 7138  cvgcmp3cetlem2 7189  cvgcmp3cet 7190  ivthlem8 7288  grpidinv 8049  spwval 8655  spwnex 8657  spwpr4OLD 8658  projlem 9212  osumlem2 9574  osumlem3 9575  osumlem4 9576  str 10179  hstr 10187  stcltrth 10200  ishoma 10686

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147

Copyright terms: Public domain