Theorem pm4.2 148

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

Assertion

Ref	Expression
pm4.2	⊢ (φ ↔ φ)

Proof of Theorem pm4.2

Step	Hyp	Ref	Expression
1		id 9	. 2 ⊢ (φ → φ)
2	1, 1	impbi 139	1 ⊢ (φ ↔ φ)

Syntax hints:   ↔ wb 127

This theorem is referenced by:  pm4.2i 149  cleqid 1102  abid2 1186  biral 1223  birex 1224  ceqsexg 1411  ru 1437  wecmpep 2193  ordon 2238  aceq1 3552  aceq5 3563  kmlem12 3591  aceqkm 3596  zorn2 3612  projlem 5224  osumlem2 5531  osumlem3 5532  osumlem4 5533  str 5698  stcltrth 5711

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

This theorem depends on definitions:  df-bi 128

metamath.org