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 1399 | . 2 ⊢ (∀𝑥𝜑 ↔ ∀𝑥𝜓) |
4 | 1, 2, 3 | 3imtr4i 199 | 1 ⊢ (𝜑 → ∀𝑥𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 ∀wal 1282 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1376 ax-gen 1378 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: hbbi 1480 hb3or 1481 hb3an 1482 hbs1f 1704 hbs1 1855 hbsbv 1858 hbeu1 1951 sb8euh 1964 hbmo1 1979 hbmo 1980 hbab1 2070 hbab 2072 cleqh 2178 hbxfreq 2185 hbral 2395 hbra1 2396 |
Copyright terms: Public domain | W3C validator |