![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3eqtr4a | GIF version |
Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
3eqtr4a.1 | ⊢ 𝐴 = 𝐵 |
3eqtr4a.2 | ⊢ (𝜑 → 𝐶 = 𝐴) |
3eqtr4a.3 | ⊢ (𝜑 → 𝐷 = 𝐵) |
Ref | Expression |
---|---|
3eqtr4a | ⊢ (𝜑 → 𝐶 = 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3eqtr4a.2 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐴) | |
2 | 3eqtr4a.1 | . . 3 ⊢ 𝐴 = 𝐵 | |
3 | 1, 2 | eqtrdi 2226 | . 2 ⊢ (𝜑 → 𝐶 = 𝐵) |
4 | 3eqtr4a.3 | . 2 ⊢ (𝜑 → 𝐷 = 𝐵) | |
5 | 3, 4 | eqtr4d 2213 | 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: uniintsnr 3878 fndmdifcom 5617 offres 6129 1stval2 6149 2ndval2 6150 ecovcom 6635 ecovass 6637 ecovdi 6639 nnnninfeq2 7120 zeo 9334 xnegneg 9807 xaddcom 9835 xaddid1 9836 xnegdi 9842 fzsuc2 10052 expnegap0 10501 facp1 10681 bcpasc 10717 hashfzp1 10775 resunimafz0 10782 absexp 11059 iooinsup 11256 fsumf1o 11369 fsumadd 11385 fisumrev2 11425 fsumparts 11449 fprodf1o 11567 fprodmul 11570 efexp 11661 tanval2ap 11692 gcdcom 11944 gcd0id 11950 dfgcd3 11981 gcdass 11986 lcmcom 12034 lcmneg 12044 lcmass 12055 sqrt2irrlem 12131 nn0gcdsq 12170 dfphi2 12190 eulerthlemth 12202 pcneg 12294 setscom 12472 restco 13307 txtopon 13395 dvef 13821 lgsneg 14058 lgsneg1 14059 lgsdir2 14067 lgsdir 14069 lgsdi 14071 |
Copyright terms: Public domain | W3C validator |