![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3eqtrrd | GIF version |
Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
3eqtrd.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
3eqtrd.2 | ⊢ (𝜑 → 𝐵 = 𝐶) |
3eqtrd.3 | ⊢ (𝜑 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
3eqtrrd | ⊢ (𝜑 → 𝐷 = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtrd.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | 3eqtrd.2 | . . 3 ⊢ (𝜑 → 𝐵 = 𝐶) | |
3 | 1, 2 | eqtrd 2220 | . 2 ⊢ (𝜑 → 𝐴 = 𝐶) |
4 | 3eqtrd.3 | . 2 ⊢ (𝜑 → 𝐶 = 𝐷) | |
5 | 3, 4 | eqtr2d 2221 | 1 ⊢ (𝜑 → 𝐷 = 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1363 |
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 1457 ax-gen 1459 ax-4 1520 ax-17 1536 ax-ext 2169 |
This theorem depends on definitions: df-bi 117 df-cleq 2180 |
This theorem is referenced by: nnanq0 7471 1idprl 7603 1idpru 7604 axcnre 7894 fseq1p1m1 10108 expmulzap 10580 expubnd 10591 subsq 10641 bcm1k 10754 bcpasc 10760 crim 10881 rereb 10886 fsumparts 11492 isumshft 11512 geosergap 11528 efsub 11703 sincossq 11770 efieq1re 11793 bezoutlema 12014 bezoutlemb 12015 eucalg 12073 phiprmpw 12236 modprmn0modprm0 12270 coprimeprodsq 12271 pythagtriplem15 12292 pythagtriplem17 12294 fldivp1 12360 1arithlem4 12378 strsetsid 12509 setsslid 12527 opprunitd 13358 cnfldsub 13751 upxp 14068 uptx 14070 lgsdilem 14724 2sqlem3 14760 |
Copyright terms: Public domain | W3C validator |