![]() |
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 2106 | . 2 ⊢ 𝐷 = 𝐴 |
4 | 3eqtr4i.2 | . 2 ⊢ 𝐶 = 𝐴 | |
5 | 3, 4 | eqtr4i 2106 | 1 ⊢ 𝐷 = 𝐶 |
Colors of variables: wff set class |
Syntax hints: = wceq 1285 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1377 ax-gen 1379 ax-4 1441 ax-17 1460 ax-ext 2065 |
This theorem depends on definitions: df-bi 115 df-cleq 2076 |
This theorem is referenced by: cbvreucsf 2976 dfif6 3371 qdass 3508 tpidm12 3510 unipr 3636 dfdm4 4576 dmun 4591 resres 4673 inres 4678 resiun1 4679 imainrect 4817 coundi 4873 coundir 4874 funopg 4985 offres 5815 mpt2mptsx 5876 cnvoprab 5908 snec 6256 halfpm6th 8395 numsucc 8674 decbin2 8775 znnen 10843 |
Copyright terms: Public domain | W3C validator |