![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > hbxfrbi | Unicode version |
Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Ref | Expression |
---|---|
hbxfrbi.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
hbxfrbi.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
hbxfrbi |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hbxfrbi.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | hbxfrbi.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | albii 1480 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 2, 3 | 3imtr4i 201 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1457 ax-gen 1459 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: hbbi 1558 hb3or 1559 hb3an 1560 hbs1f 1791 hbs1 1949 hbsbv 1952 hbeu1 2047 sb8euh 2060 hbmo1 2075 hbmo 2076 hbab1 2177 hbab 2179 cleqh 2288 hbxfreq 2295 hbral 2518 hbra1 2519 |
Copyright terms: Public domain | W3C validator |