pm4.2 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem pm4.2 170

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 59	. 2
2	1, 1	impbi 157	1

Colors of variables: wff set class

Syntax hints:

wb 146

This theorem is referenced by: pm4.2i 171 pm5.19 667 3anbi1i 822 3anbi2i 823 3anbi3i 824 eqid 1468 abid2 1572 ralbii 1659 rexbii 1660 ceqsexg 1878 wecmpep 2931 ordon 2977 aceq5 4712 aceqkm 4753 zorn 4769 elfz2nn0t 6427 climadd 7053 climmul 7064 climcmp 7074 cvgcmp3cetlem2 7125 cvgcmp3cet 7126 ivthlem8 7223 ivthlem8OLD 7232 grpidinv 7986 spwval 8582 projlem 9133 osumlem2 9496 osumlem3 9497 osumlem4 9498 str 10094 hstr 10102 stcltrth 10115 ishoma 10559

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