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 1741 | . 2 | |
2 | sbequ2 1742 | . 2 | |
3 | 1, 2 | impbid 128 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wsb 1735 |
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-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 |
This theorem depends on definitions: df-bi 116 df-sb 1736 |
This theorem is referenced by: sbequ12r 1745 sbequ12a 1746 sbid 1747 ax16 1785 sb8h 1826 sb8eh 1827 sb8 1828 sb8e 1829 ax16ALT 1831 sbco 1939 sbcomxyyz 1943 sb9v 1951 sb6a 1961 mopick 2075 clelab 2263 sbab 2265 cbvralf 2646 cbvrexf 2647 cbvralsv 2663 cbvrexsv 2664 cbvrab 2679 sbhypf 2730 mob2 2859 reu2 2867 reu6 2868 sbcralt 2980 sbcrext 2981 sbcralg 2982 sbcreug 2984 cbvreucsf 3059 cbvrabcsf 3060 cbvopab1 3996 cbvopab1s 3998 csbopabg 4001 cbvmptf 4017 cbvmpt 4018 opelopabsb 4177 frind 4269 tfis 4492 findes 4512 opeliunxp 4589 ralxpf 4680 rexxpf 4681 cbviota 5088 csbiotag 5111 cbvriota 5733 csbriotag 5735 abrexex2g 6011 opabex3d 6012 opabex3 6013 abrexex2 6015 dfoprab4f 6084 finexdc 6789 ssfirab 6815 uzind4s 9378 zsupcllemstep 11627 bezoutlemmain 11675 cbvrald 12984 bj-bdfindes 13136 bj-findes 13168 |
Copyright terms: Public domain | W3C validator |