![]() |
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 2111 | . 2 ⊢ 𝐷 = 𝐴 |
4 | 3eqtr4i.2 | . 2 ⊢ 𝐶 = 𝐴 | |
5 | 3, 4 | eqtr4i 2111 | 1 ⊢ 𝐷 = 𝐶 |
Colors of variables: wff set class |
Syntax hints: = wceq 1289 |
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 1381 ax-gen 1383 ax-4 1445 ax-17 1464 ax-ext 2070 |
This theorem depends on definitions: df-bi 115 df-cleq 2081 |
This theorem is referenced by: cbvreucsf 2992 dfif6 3395 qdass 3539 tpidm12 3541 unipr 3667 dfdm4 4628 dmun 4643 resres 4725 inres 4730 resdifcom 4731 resiun1 4732 imainrect 4876 coundi 4932 coundir 4933 funopg 5048 offres 5906 mpt2mptsx 5967 cnvoprab 5999 snec 6351 halfpm6th 8634 numsucc 8914 decbin2 9015 fsumadd 10796 fsum2d 10825 znnen 11485 |
Copyright terms: Public domain | W3C validator |