![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sylan9eq | Unicode version |
Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
sylan9eq.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
sylan9eq.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
sylan9eq |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylan9eq.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sylan9eq.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | eqtr 2112 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | syl2an 284 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1388 ax-gen 1390 ax-4 1452 ax-17 1471 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-cleq 2088 |
This theorem is referenced by: sylan9req 2148 sylan9eqr 2149 difeq12 3128 uneq12 3164 ineq12 3211 ifeq12 3427 preq12 3541 prprc 3572 preq12b 3636 opeq12 3646 xpeq12 4486 nfimad 4816 coi2 4981 funimass1 5125 f1orescnv 5304 resdif 5310 oveq12 5699 cbvmpt2v 5766 ovmpt2g 5817 eqopi 5980 fmpt2co 6019 nnaordex 6326 map0g 6485 xpcomco 6622 xpmapenlem 6645 phplem3 6650 phplem4 6651 sbthlemi5 6750 addcmpblnq 7023 ltrnqg 7076 enq0ref 7089 addcmpblnq0 7099 distrlem4prl 7240 distrlem4pru 7241 recexgt0sr 7416 axcnre 7513 cnegexlem2 7755 cnegexlem3 7756 recexap 8219 xaddpnf2 9413 xaddmnf2 9415 rexadd 9418 xaddnemnf 9423 xaddnepnf 9424 xposdif 9448 frec2uzrand 9961 seqeq3 10005 shftcan1 10383 remul2 10422 immul2 10429 ef0lem 11099 efieq1re 11210 dvdsnegb 11240 dvdscmul 11250 dvds2ln 11256 dvds2add 11257 dvds2sub 11258 gcdn0val 11380 rpmulgcd 11442 lcmval 11472 lcmn0val 11475 isopn3 11977 |
Copyright terms: Public domain | W3C validator |