| 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 2253 | . 2 ⊢ (𝜑 → 𝐶 = 𝐵) |
| 4 | 3eqtr4a.3 | . 2 ⊢ (𝜑 → 𝐷 = 𝐵) | |
| 5 | 3, 4 | eqtr4d 2240 | 1 ⊢ (𝜑 → 𝐶 = 𝐷) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 = wceq 1372 |
| 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 1469 ax-gen 1471 ax-4 1532 ax-17 1548 ax-ext 2186 |
| This theorem depends on definitions: df-bi 117 df-cleq 2197 |
| This theorem is referenced by: uniintsnr 3920 fndmdifcom 5680 offres 6210 1stval2 6231 2ndval2 6232 ecovcom 6719 ecovass 6721 ecovdi 6723 nnnninfeq2 7213 zeo 9460 xnegneg 9937 xaddcom 9965 xaddid1 9966 xnegdi 9972 fzsuc2 10183 expnegap0 10673 facp1 10856 bcpasc 10892 hashfzp1 10950 resunimafz0 10957 absexp 11309 iooinsup 11507 fsumf1o 11620 fsumadd 11636 fisumrev2 11676 fsumparts 11700 fprodf1o 11818 fprodmul 11821 efexp 11912 tanval2ap 11943 gcdcom 12213 gcd0id 12219 dfgcd3 12250 gcdass 12255 lcmcom 12305 lcmneg 12315 lcmass 12326 sqrt2irrlem 12402 nn0gcdsq 12441 dfphi2 12461 eulerthlemth 12473 pcneg 12567 setscom 12791 gsumfzfsumlem0 14266 restco 14564 txtopon 14652 dvmptid 15106 dvef 15117 fsumdvdsmul 15381 lgsneg 15419 lgsneg1 15420 lgsdir2 15428 lgsdir 15430 lgsdi 15432 lgsquad2lem2 15477 |
| Copyright terms: Public domain | W3C validator |