![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3eqtr4ri | GIF version |
Description: An inference from three chained equalities. (Contributed by NM, 2-Sep-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
3eqtr4i.1 | ⊢ 𝐴 = 𝐵 |
3eqtr4i.2 | ⊢ 𝐶 = 𝐴 |
3eqtr4i.3 | ⊢ 𝐷 = 𝐵 |
Ref | Expression |
---|---|
3eqtr4ri | ⊢ 𝐷 = 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr4i.3 | . . 3 ⊢ 𝐷 = 𝐵 | |
2 | 3eqtr4i.1 | . . 3 ⊢ 𝐴 = 𝐵 | |
3 | 1, 2 | eqtr4i 2201 | . 2 ⊢ 𝐷 = 𝐴 |
4 | 3eqtr4i.2 | . 2 ⊢ 𝐶 = 𝐴 | |
5 | 3, 4 | eqtr4i 2201 | 1 ⊢ 𝐷 = 𝐶 |
Colors of variables: wff set class |
Syntax hints: = 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: cbvreucsf 3121 dfif6 3536 qdass 3689 tpidm12 3691 unipr 3823 dfdm4 4819 dmun 4834 resres 4919 inres 4924 resdifcom 4925 resiun1 4926 imainrect 5074 coundi 5130 coundir 5131 funopg 5250 offres 6135 mpomptsx 6197 cnvoprab 6234 snec 6595 halfpm6th 9138 numsucc 9422 decbin2 9523 fsumadd 11413 fsum2d 11442 fprodmul 11598 fprodfac 11622 fprodrec 11636 znnen 12398 |
Copyright terms: Public domain | W3C validator |