New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > 3eqtr3i | GIF version |
Description: An inference from three chained equalities. (Contributed by NM, 6-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
3eqtr3i.1 | ⊢ A = B |
3eqtr3i.2 | ⊢ A = C |
3eqtr3i.3 | ⊢ B = D |
Ref | Expression |
---|---|
3eqtr3i | ⊢ C = D |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr3i.1 | . . 3 ⊢ A = B | |
2 | 3eqtr3i.2 | . . 3 ⊢ A = C | |
3 | 1, 2 | eqtr3i 2375 | . 2 ⊢ B = C |
4 | 3eqtr3i.3 | . 2 ⊢ B = D | |
5 | 3, 4 | eqtr3i 2375 | 1 ⊢ C = D |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1642 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-11 1746 ax-ext 2334 |
This theorem depends on definitions: df-bi 177 df-ex 1542 df-cleq 2346 |
This theorem is referenced by: csbvarg 3163 un12 3421 in12 3466 indif1 3499 difundi 3507 difundir 3508 difindi 3509 difindir 3510 dif32 3517 undif1 3625 addc4 4417 addc6 4418 tfin1c 4499 xp0 5044 caov12 5636 caov13 5638 caov411 5640 caovdir 5642 tcdi 6164 tc2c 6166 ce0addcnnul 6179 nchoicelem1 6289 |
Copyright terms: Public domain | W3C validator |