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 | syl6eq 2166 | . 2 ⊢ (𝜑 → 𝐶 = 𝐵) |
4 | 3eqtr4a.3 | . 2 ⊢ (𝜑 → 𝐷 = 𝐵) | |
5 | 3, 4 | eqtr4d 2153 | 1 ⊢ (𝜑 → 𝐶 = 𝐷) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1316 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1408 ax-gen 1410 ax-4 1472 ax-17 1491 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-cleq 2110 |
This theorem is referenced by: uniintsnr 3777 fndmdifcom 5494 offres 6001 1stval2 6021 2ndval2 6022 ecovcom 6504 ecovass 6506 ecovdi 6508 zeo 9124 xnegneg 9584 xaddcom 9612 xaddid1 9613 xnegdi 9619 fzsuc2 9827 expnegap0 10269 facp1 10444 bcpasc 10480 hashfzp1 10538 resunimafz0 10542 absexp 10819 iooinsup 11014 fsumf1o 11127 fsumadd 11143 fisumrev2 11183 fsumparts 11207 efexp 11315 tanval2ap 11347 gcdcom 11589 gcd0id 11594 dfgcd3 11625 gcdass 11630 lcmcom 11672 lcmneg 11682 lcmass 11693 sqrt2irrlem 11766 nn0gcdsq 11805 dfphi2 11823 setscom 11926 restco 12270 txtopon 12358 dvef 12783 |
Copyright terms: Public domain | W3C validator |