Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eqtr2id | GIF version |
Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.) |
Ref | Expression |
---|---|
eqtr2id.1 | ⊢ 𝐴 = 𝐵 |
eqtr2id.2 | ⊢ (𝜑 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
eqtr2id | ⊢ (𝜑 → 𝐶 = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqtr2id.1 | . . 3 ⊢ 𝐴 = 𝐵 | |
2 | eqtr2id.2 | . . 3 ⊢ (𝜑 → 𝐵 = 𝐶) | |
3 | 1, 2 | eqtrid 2216 | . 2 ⊢ (𝜑 → 𝐴 = 𝐶) |
4 | 3 | eqcomd 2177 | 1 ⊢ (𝜑 → 𝐶 = 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1349 |
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-5 1441 ax-gen 1443 ax-4 1504 ax-17 1520 ax-ext 2153 |
This theorem depends on definitions: df-bi 116 df-cleq 2164 |
This theorem is referenced by: eqtr3di 2219 opeqsn 4238 dcextest 4566 relop 4762 funopg 5234 funcnvres 5273 mapsnconst 6676 snexxph 6931 apreap 8510 recextlem1 8573 nn0supp 9191 intqfrac2 10279 hashprg 10747 hashfacen 10775 explecnv 11472 grp1inv 12810 rerestcntop 13429 binom4 13776 |
Copyright terms: Public domain | W3C validator |