![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3eqtr3rd | GIF version |
Description: A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.) |
Ref | Expression |
---|---|
3eqtr3d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
3eqtr3d.2 | ⊢ (𝜑 → 𝐴 = 𝐶) |
3eqtr3d.3 | ⊢ (𝜑 → 𝐵 = 𝐷) |
Ref | Expression |
---|---|
3eqtr3rd | ⊢ (𝜑 → 𝐷 = 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr3d.3 | . 2 ⊢ (𝜑 → 𝐵 = 𝐷) | |
2 | 3eqtr3d.1 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐵) | |
3 | 3eqtr3d.2 | . . 3 ⊢ (𝜑 → 𝐴 = 𝐶) | |
4 | 2, 3 | eqtr3d 2212 | . 2 ⊢ (𝜑 → 𝐵 = 𝐶) |
5 | 1, 4 | eqtr3d 2212 | 1 ⊢ (𝜑 → 𝐷 = 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = 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: fcofo 5788 fcof1o 5793 frecabcl 6403 nnaword 6515 nninfisol 7134 enomnilem 7139 fodju0 7148 enmkvlem 7162 enwomnilem 7170 pn0sr 7773 negeu 8151 add20 8434 2halves 9151 bcnn 10740 bcpasc 10749 resqrexlemover 11022 fsumneg 11462 geolim 11522 geolim2 11523 mertensabs 11548 sincossq 11759 demoivre 11783 eirraplem 11787 gcdid 11990 gcdmultipled 11997 phiprmpw 12225 pythagtriplem12 12278 expnprm 12354 imasbas 12734 imasplusg 12735 imasmulr 12736 grpinvid1 12931 grpnpcan 12969 grplactcnv 12979 ghmgrp 12991 ringnegl 13239 ringnegr 13240 ringmneg2 13242 ring1 13247 rdivmuldivd 13324 lmodfopne 13427 lmodvsneg 13432 ioo2bl 14204 ptolemy 14406 coskpi 14430 logbgcd1irr 14546 logbgcd1irraplemap 14548 |
Copyright terms: Public domain | W3C validator |