![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > suceq | Unicode version |
Description: Equality of successors. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Ref | Expression |
---|---|
suceq |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sneq 3504 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | uneq12d 3197 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | df-suc 4253 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | df-suc 4253 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 3, 4, 5 | 3eqtr4g 2172 |
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-io 681 ax-5 1406 ax-7 1407 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-8 1465 ax-10 1466 ax-11 1467 ax-i12 1468 ax-bndl 1469 ax-4 1470 ax-17 1489 ax-i9 1493 ax-ial 1497 ax-i5r 1498 ax-ext 2097 |
This theorem depends on definitions: df-bi 116 df-tru 1317 df-nf 1420 df-sb 1719 df-clab 2102 df-cleq 2108 df-clel 2111 df-nfc 2244 df-v 2659 df-un 3041 df-sn 3499 df-suc 4253 |
This theorem is referenced by: eqelsuc 4301 2ordpr 4399 onsucsssucexmid 4402 onsucelsucexmid 4405 ordsucunielexmid 4406 suc11g 4432 onsucuni2 4439 0elsucexmid 4440 ordpwsucexmid 4445 peano2 4469 findes 4477 nn0suc 4478 0elnn 4492 omsinds 4495 tfr1onlemsucaccv 6192 tfrcllemsucaccv 6205 tfrcl 6215 frecabcl 6250 frecsuc 6258 sucinc 6295 sucinc2 6296 oacl 6310 oav2 6313 oasuc 6314 oa1suc 6317 nna0r 6328 nnacom 6334 nnaass 6335 nnmsucr 6338 nnsucelsuc 6341 nnsucsssuc 6342 nnaword 6361 nnaordex 6377 phplem3g 6703 nneneq 6704 php5 6705 php5dom 6710 omp1eomlem 6931 omp1eom 6932 indpi 7098 ennnfoneleminc 11769 ennnfonelemex 11772 bj-indsuc 12818 bj-bdfindes 12839 bj-nn0suc0 12840 bj-peano4 12845 bj-inf2vnlem1 12860 bj-nn0sucALT 12868 bj-findes 12871 nnsf 12891 nninfalllemn 12894 nninfsellemdc 12898 nninfself 12901 nninfsellemeqinf 12904 nninfomni 12907 |
Copyright terms: Public domain | W3C validator |