![]() |
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 3114 disjdif2 3503 dfopg 3778 xpid11 4852 sqxpeq0 5054 cores2 5143 funcoeqres 5494 dftpos2 6265 ine0 8354 fisumcom2 11449 fisum0diag2 11458 mertenslemi1 11546 fprodcom2fi 11637 fprodmodd 11652 4sqlem10 12388 setsslnid 12517 xpsff1o 12774 eqglact 13090 oppr1g 13258 dvmptccn 14319 nninffeq 14909 |
Copyright terms: Public domain | W3C validator |