![]() |
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 2105 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 1, 2, 3 | syl2an 283 |
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 104 ax-ia2 105 ax-ia3 106 ax-5 1381 ax-gen 1383 ax-4 1445 ax-17 1464 ax-ext 2070 |
This theorem depends on definitions: df-bi 115 df-cleq 2081 |
This theorem is referenced by: sylan9req 2141 sylan9eqr 2142 difeq12 3113 uneq12 3149 ineq12 3196 ifeq12 3407 preq12 3521 prprc 3552 preq12b 3614 opeq12 3624 xpeq12 4457 nfimad 4783 coi2 4947 funimass1 5091 f1orescnv 5269 resdif 5275 oveq12 5661 cbvmpt2v 5728 ovmpt2g 5779 eqopi 5942 fmpt2co 5981 nnaordex 6284 map0g 6443 xpcomco 6540 xpmapenlem 6563 phplem3 6568 phplem4 6569 sbthlemi5 6668 addcmpblnq 6924 ltrnqg 6977 enq0ref 6990 addcmpblnq0 7000 distrlem4prl 7141 distrlem4pru 7142 recexgt0sr 7317 axcnre 7414 cnegexlem2 7656 cnegexlem3 7657 recexap 8120 frec2uzrand 9808 iseqeq3 9856 shftcan1 10264 remul2 10303 immul2 10310 ef0lem 10946 efieq1re 11057 dvdsnegb 11087 dvdscmul 11097 dvds2ln 11103 dvds2add 11104 dvds2sub 11105 gcdn0val 11227 rpmulgcd 11289 lcmval 11319 lcmn0val 11322 |
Copyright terms: Public domain | W3C validator |