![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > equequ2 | GIF version |
Description: An equivalence law for equality. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
equequ2 | ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equtrr 1687 | . 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦)) | |
2 | equtrr 1687 | . . 3 ⊢ (𝑦 = 𝑥 → (𝑧 = 𝑦 → 𝑧 = 𝑥)) | |
3 | 2 | equcoms 1685 | . 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑦 → 𝑧 = 𝑥)) |
4 | 1, 3 | impbid 128 | 1 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-gen 1426 ax-ie2 1471 ax-8 1483 ax-17 1507 ax-i9 1511 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: ax11v2 1793 ax11v 1800 ax11ev 1801 equs5or 1803 eujust 2002 euf 2005 mo23 2041 eleq1w 2201 disjiun 3932 iotaval 5107 dffun4f 5147 dff13f 5679 supmoti 6888 isoti 6902 ennnfonelemr 11972 ctinf 11979 |
Copyright terms: Public domain | W3C validator |