![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sbequ12 | Unicode version |
Description: An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
sbequ12 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbequ1 1648 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sbequ2 1649 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | impbid 120 |
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 99 ax-ia2 100 ax-ia3 101 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-4 1397 |
This theorem depends on definitions: df-bi 110 df-sb 1643 |
This theorem is referenced by: sbequ12r 1652 sbequ12a 1653 sbid 1654 ax16 1691 sb8h 1731 sb8eh 1732 sb8 1733 sb8e 1734 ax16ALT 1736 sbco 1839 sbcomxyyz 1843 sb9v 1851 sb6a 1861 mopick 1975 clelab 2159 sbab 2161 cbvralf 2521 cbvrexf 2522 cbvralsv 2538 cbvrexsv 2539 cbvrab 2549 sbhypf 2597 mob2 2715 reu2 2723 reu6 2724 sbcralt 2828 sbcrext 2829 sbcralg 2830 sbcrexg 2831 sbcreug 2832 cbvreucsf 2904 cbvrabcsf 2905 cbvopab1 3821 cbvopab1s 3823 csbopabg 3826 cbvmpt 3842 opelopabsb 3988 tfis 4249 findes 4269 opeliunxp 4338 ralxpf 4425 rexxpf 4426 cbviota 4815 csbiotag 4838 cbvriota 5421 csbriotag 5423 abrexex2g 5689 opabex3d 5690 opabex3 5691 abrexex2 5693 dfoprab4f 5761 uzind4s 8309 cbvrald 9262 bj-bdfindes 9409 bj-findes 9441 |
Copyright terms: Public domain | W3C validator |