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 1671 | . 2 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 → 𝑧 = 𝑦)) | |
2 | equtrr 1671 | . . 3 ⊢ (𝑦 = 𝑥 → (𝑧 = 𝑦 → 𝑧 = 𝑥)) | |
3 | 2 | equcoms 1669 | . 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 1410 ax-ie2 1455 ax-8 1467 ax-17 1491 ax-i9 1495 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: ax11v2 1776 ax11v 1783 ax11ev 1784 equs5or 1786 eujust 1979 euf 1982 mo23 2018 eleq1w 2178 disjiun 3894 iotaval 5069 dffun4f 5109 dff13f 5639 supmoti 6848 isoti 6862 ennnfonelemr 11863 ctinf 11870 |
Copyright terms: Public domain | W3C validator |