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 2215 | . 2 ⊢ (𝜑 → 𝐴 = 𝐶) |
4 | 3 | eqcomd 2176 | 1 ⊢ (𝜑 → 𝐶 = 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1348 |
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 1440 ax-gen 1442 ax-4 1503 ax-17 1519 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-cleq 2163 |
This theorem is referenced by: eqtr3di 2218 opeqsn 4235 dcextest 4563 relop 4759 funopg 5230 funcnvres 5269 mapsnconst 6668 snexxph 6923 apreap 8493 recextlem1 8556 nn0supp 9174 intqfrac2 10262 hashprg 10730 hashfacen 10758 explecnv 11455 rerestcntop 13265 binom4 13612 |
Copyright terms: Public domain | W3C validator |