Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > hbxfrbi | GIF 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 1431 | . 2 ⊢ (∀𝑥𝜑 ↔ ∀𝑥𝜓) |
4 | 1, 2, 3 | 3imtr4i 200 | 1 ⊢ (𝜑 → ∀𝑥𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 ∀wal 1314 |
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 1408 ax-gen 1410 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: hbbi 1512 hb3or 1513 hb3an 1514 hbs1f 1739 hbs1 1891 hbsbv 1894 hbeu1 1987 sb8euh 2000 hbmo1 2015 hbmo 2016 hbab1 2106 hbab 2108 cleqh 2217 hbxfreq 2224 hbral 2441 hbra1 2442 |
Copyright terms: Public domain | W3C validator |