![]() |
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 2213 | . 2 ⊢ 𝐷 = 𝐴 |
4 | 3eqtr4i.2 | . 2 ⊢ 𝐶 = 𝐴 | |
5 | 3, 4 | eqtr4i 2213 | 1 ⊢ 𝐷 = 𝐶 |
Colors of variables: wff set class |
Syntax hints: = wceq 1364 |
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 1458 ax-gen 1460 ax-4 1521 ax-17 1537 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-cleq 2182 |
This theorem is referenced by: cbvreucsf 3136 dfif6 3551 qdass 3704 tpidm12 3706 unipr 3838 dfdm4 4837 dmun 4852 resres 4937 inres 4942 resdifcom 4943 resiun1 4944 imainrect 5092 coundi 5148 coundir 5149 funopg 5269 offres 6160 mpomptsx 6222 cnvoprab 6259 snec 6622 halfpm6th 9169 numsucc 9453 decbin2 9554 fsumadd 11446 fsum2d 11475 fprodmul 11631 fprodfac 11655 fprodrec 11669 znnen 12449 |
Copyright terms: Public domain | W3C validator |