Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sbequ | Unicode version |
Description: An equality theorem for substitution. Used in proof of Theorem 9.7 in [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
sbequ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbequi 1795 | . 2 | |
2 | sbequi 1795 | . . 3 | |
3 | 2 | equcoms 1669 | . 2 |
4 | 1, 3 | impbid 128 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wsb 1720 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 683 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-10 1468 ax-11 1469 ax-i12 1470 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-sb 1721 |
This theorem is referenced by: drsb2 1797 sbco2vlem 1897 sbco2yz 1914 sbcocom 1921 sb10f 1948 hbsb4 1965 nfsb4or 1976 sb8eu 1990 sb8euh 2000 cbvab 2240 cbvralf 2625 cbvrexf 2626 cbvreu 2629 cbvralsv 2642 cbvrexsv 2643 cbvrab 2658 cbvreucsf 3034 cbvrabcsf 3035 sbss 3441 disjiun 3894 cbvopab1 3971 cbvmpt 3993 tfis 4467 findes 4487 cbviota 5063 sb8iota 5065 cbvriota 5708 uzind4s 9353 bezoutlemmain 11613 cbvrald 12922 setindft 13090 |
Copyright terms: Public domain | W3C validator |