![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqeq2 | GIF version |
Description: Equality implies equivalence of equalities. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eqeq2 | ⊢ (A = B → (𝐶 = A ↔ 𝐶 = B)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq1 2043 | . 2 ⊢ (A = B → (A = 𝐶 ↔ B = 𝐶)) | |
2 | eqcom 2039 | . 2 ⊢ (𝐶 = A ↔ A = 𝐶) | |
3 | eqcom 2039 | . 2 ⊢ (𝐶 = B ↔ B = 𝐶) | |
4 | 1, 2, 3 | 3bitr4g 212 | 1 ⊢ (A = B → (𝐶 = A ↔ 𝐶 = B)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 = wceq 1242 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 ax-4 1397 ax-17 1416 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-cleq 2030 |
This theorem is referenced by: eqeq2i 2047 eqeq2d 2048 eqeq12 2049 eleq1 2097 neeq2 2214 alexeq 2664 ceqex 2665 pm13.183 2675 eqeu 2705 mo2icl 2714 mob2 2715 euind 2722 reu6i 2726 reuind 2738 sbc5 2781 csbiebg 2883 sneq 3378 preqr1g 3528 preqr1 3530 prel12 3533 preq12bg 3535 opth 3965 euotd 3982 ordtriexmid 4210 tfisi 4253 ideqg 4430 resieq 4565 cnveqb 4719 cnveq0 4720 iota5 4830 funopg 4877 fneq2 4931 foeq3 5047 tz6.12f 5145 funbrfv 5155 fnbrfvb 5157 fvelimab 5172 elrnrexdm 5249 eufnfv 5332 f1veqaeq 5351 mpt2eq123 5506 ovmpt4g 5565 ovi3 5579 ovg 5581 caovcang 5604 caovcan 5607 nntri3or 6011 nnaordex 6036 nnawordex 6037 ereq2 6050 eroveu 6133 2dom 6221 fundmen 6222 nqtri3or 6380 ltexnqq 6391 aptisr 6705 axpre-apti 6769 subval 7000 divvalap 7435 nn0ind-raph 8131 frecuzrdgfn 8879 sqrtrval 9209 |
Copyright terms: Public domain | W3C validator |