![]() |
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 3123 dfif6 3538 qdass 3691 tpidm12 3693 unipr 3825 dfdm4 4821 dmun 4836 resres 4921 inres 4926 resdifcom 4927 resiun1 4928 imainrect 5076 coundi 5132 coundir 5133 funopg 5252 offres 6138 mpomptsx 6200 cnvoprab 6237 snec 6598 halfpm6th 9141 numsucc 9425 decbin2 9526 fsumadd 11416 fsum2d 11445 fprodmul 11601 fprodfac 11625 fprodrec 11639 znnen 12401 |
Copyright terms: Public domain | W3C validator |