![]() |
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 3605 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | uneq12d 3292 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | df-suc 4373 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | df-suc 4373 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 3, 4, 5 | 3eqtr4g 2235 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
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-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-v 2741 df-un 3135 df-sn 3600 df-suc 4373 |
This theorem is referenced by: eqelsuc 4421 2ordpr 4525 onsucsssucexmid 4528 onsucelsucexmid 4531 ordsucunielexmid 4532 suc11g 4558 onsucuni2 4565 0elsucexmid 4566 ordpwsucexmid 4571 peano2 4596 findes 4604 nn0suc 4605 0elnn 4620 omsinds 4623 tfr1onlemsucaccv 6345 tfrcllemsucaccv 6358 tfrcl 6368 frecabcl 6403 frecsuc 6411 sucinc 6449 sucinc2 6450 oacl 6464 oav2 6467 oasuc 6468 oa1suc 6471 nna0r 6482 nnacom 6488 nnaass 6489 nnmsucr 6492 nnsucelsuc 6495 nnsucsssuc 6496 nnaword 6515 nnaordex 6532 phplem3g 6859 nneneq 6860 php5 6861 php5dom 6866 omp1eomlem 7096 omp1eom 7097 nnnninfeq 7129 nnnninfeq2 7130 nninfwlpoimlemg 7176 nninfwlpoimlemginf 7177 nninfwlpoim 7179 indpi 7344 ennnfoneleminc 12415 ennnfonelemex 12418 bj-indsuc 14868 bj-bdfindes 14889 bj-nn0suc0 14890 bj-peano4 14895 bj-inf2vnlem1 14910 bj-nn0sucALT 14918 bj-findes 14921 nnsf 14943 nninfsellemdc 14948 nninfself 14951 nninfsellemeqinf 14954 nninfomni 14957 |
Copyright terms: Public domain | W3C validator |