![]() |
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 1427 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 2, 3 | 3imtr4i 200 |
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 105 ax-ia2 106 ax-ia3 107 ax-5 1404 ax-gen 1406 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: hbbi 1508 hb3or 1509 hb3an 1510 hbs1f 1735 hbs1 1887 hbsbv 1890 hbeu1 1983 sb8euh 1996 hbmo1 2011 hbmo 2012 hbab1 2102 hbab 2104 cleqh 2212 hbxfreq 2219 hbral 2436 hbra1 2437 |
Copyright terms: Public domain | W3C validator |