Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sb2 | Unicode version |
Description: One direction of a simplified definition of substitution. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
sb2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-4 1497 | . 2 | |
2 | equs4 1712 | . 2 | |
3 | df-sb 1750 | . 2 | |
4 | 1, 2, 3 | sylanbrc 414 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wal 1340 wex 1479 wsb 1749 |
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-5 1434 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-4 1497 ax-i9 1517 ax-ial 1521 |
This theorem depends on definitions: df-bi 116 df-sb 1750 |
This theorem is referenced by: stdpc4 1762 equsb1 1772 equsb2 1773 sbiedh 1774 sb6f 1790 hbsb2a 1793 hbsb2e 1794 sbcof2 1797 sb3 1818 sb4b 1821 sb4bor 1822 hbsb2 1823 nfsb2or 1824 sb6rf 1840 sbi1v 1878 sbalyz 1986 iota4 5165 |
Copyright terms: Public domain | W3C validator |