![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3eqtr3g | GIF version |
Description: A chained equality inference, useful for converting from definitions. (Contributed by NM, 15-Nov-1994.) |
Ref | Expression |
---|---|
3eqtr3g.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
3eqtr3g.2 | ⊢ 𝐴 = 𝐶 |
3eqtr3g.3 | ⊢ 𝐵 = 𝐷 |
Ref | Expression |
---|---|
3eqtr3g | ⊢ (𝜑 → 𝐶 = 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr3g.2 | . . 3 ⊢ 𝐴 = 𝐶 | |
2 | 3eqtr3g.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
3 | 1, 2 | eqtr3id 2224 | . 2 ⊢ (𝜑 → 𝐶 = 𝐵) |
4 | 3eqtr3g.3 | . 2 ⊢ 𝐵 = 𝐷 | |
5 | 3, 4 | eqtrdi 2226 | 1 ⊢ (𝜑 → 𝐶 = 𝐷) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1353 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-4 1510 ax-17 1526 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-cleq 2170 |
This theorem is referenced by: csbnest1g 3112 disjdif2 3501 dfopg 3776 xpid11 4850 sqxpeq0 5052 cores2 5141 funcoeqres 5492 dftpos2 6261 ine0 8349 fisumcom2 11441 fisum0diag2 11450 mertenslemi1 11538 fprodcom2fi 11629 fprodmodd 11644 4sqlem10 12379 setsslnid 12508 eqglact 13037 oppr1g 13205 dvmptccn 14072 nninffeq 14651 |
Copyright terms: Public domain | W3C validator |