Metamath Proof Explorer
Table of Contents - 20.4.16. Well-founded induction
- bnj1204
- bnj1234
- bnj1245
- bnj1256
- bnj1259
- bnj1253
- bnj1279
- bnj1286
- bnj1280
- bnj1296
- bnj1309
- bnj1307
- bnj1311
- bnj1318
- bnj1326
- bnj1321
- bnj1364
- bnj1371
- bnj1373
- bnj1374
- bnj1384
- bnj1388
- bnj1398
- bnj1413
- bnj1408
- bnj1414
- bnj1415
- bnj1416
- bnj1418
- bnj1417
- bnj1421
- bnj1444
- bnj1445
- bnj1446
- bnj1447
- bnj1448
- bnj1449
- bnj1442
- bnj1450
- bnj1423
- bnj1452
- bnj1466
- bnj1467
- bnj1463
- bnj1489
- bnj1491
- bnj1312
- bnj1493
- bnj1497
- bnj1498