![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3eqtr3a | GIF version |
Description: A chained equality inference, useful for converting from definitions. (Contributed by Mario Carneiro, 6-Nov-2015.) |
Ref | Expression |
---|---|
3eqtr3a.1 | ⊢ 𝐴 = 𝐵 |
3eqtr3a.2 | ⊢ (𝜑 → 𝐴 = 𝐶) |
3eqtr3a.3 | ⊢ (𝜑 → 𝐵 = 𝐷) |
Ref | Expression |
---|---|
3eqtr3a | ⊢ (𝜑 → 𝐶 = 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr3a.2 | . 2 ⊢ (𝜑 → 𝐴 = 𝐶) | |
2 | 3eqtr3a.1 | . . 3 ⊢ 𝐴 = 𝐵 | |
3 | 3eqtr3a.3 | . . 3 ⊢ (𝜑 → 𝐵 = 𝐷) | |
4 | 2, 3 | eqtrid 2222 | . 2 ⊢ (𝜑 → 𝐴 = 𝐷) |
5 | 1, 4 | eqtr3d 2212 | 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: uneqin 3386 coi2 5145 foima 5443 f1imacnv 5478 fvsnun2 5714 fnsnsplitdc 6505 phplem4 6854 phplem4on 6866 halfnqq 7408 resqrexlemcalc1 11018 absefib 11773 efieq1re 11774 restopnb 13612 cnmpt2t 13724 reeflog 14215 rpcxpsqrt 14273 |
Copyright terms: Public domain | W3C validator |