![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl6eqr | GIF version |
Description: An equality transitivity deduction. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
syl6eqr.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
syl6eqr.2 | ⊢ 𝐶 = 𝐵 |
Ref | Expression |
---|---|
syl6eqr | ⊢ (𝜑 → 𝐴 = 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6eqr.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | syl6eqr.2 | . . 3 ⊢ 𝐶 = 𝐵 | |
3 | 2 | eqcomi 2044 | . 2 ⊢ 𝐵 = 𝐶 |
4 | 1, 3 | syl6eq 2088 | 1 ⊢ (𝜑 → 𝐴 = 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1243 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-4 1400 ax-17 1419 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-cleq 2033 |
This theorem is referenced by: 3eqtr4g 2097 rabxmdc 3249 relop 4486 csbcnvg 4519 dfiun3g 4589 dfiin3g 4590 resima2 4644 relcnvfld 4851 uniabio 4877 fntpg 4955 dffn5im 5219 dfimafn2 5223 fncnvima2 5288 fmptcof 5331 fcoconst 5334 fnasrng 5343 ffnov 5605 fnovim 5609 fnrnov 5646 foov 5647 funimassov 5650 ovelimab 5651 ofc12 5731 caofinvl 5733 dftpos3 5877 tfr0 5937 rdgisucinc 5972 oasuc 6044 ecinxp 6181 phplem1 6315 indpi 6440 nqnq0pi 6536 nq0m0r 6554 addnqpr1 6660 recexgt0sr 6858 recidpipr 6932 recidpirq 6934 axrnegex 6953 nntopi 6968 cnref1o 8582 fztp 8940 fseq1m1p1 8957 frecuzrdgrrn 9194 frecuzrdgsuc 9201 mulexpzap 9295 expaddzap 9299 cjexp 9493 rexuz3 9588 climconst 9811 |
Copyright terms: Public domain | W3C validator |