Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfxfrd | GIF version |
Description: A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Ref | Expression |
---|---|
nfbii.1 | ⊢ (𝜑 ↔ 𝜓) |
nfxfrd.2 | ⊢ (𝜒 → Ⅎ𝑥𝜓) |
Ref | Expression |
---|---|
nfxfrd | ⊢ (𝜒 → Ⅎ𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfxfrd.2 | . 2 ⊢ (𝜒 → Ⅎ𝑥𝜓) | |
2 | nfbii.1 | . . 3 ⊢ (𝜑 ↔ 𝜓) | |
3 | 2 | nfbii 1362 | . 2 ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓) |
4 | 1, 3 | sylibr 137 | 1 ⊢ (𝜒 → Ⅎ𝑥𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 Ⅎwnf 1349 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 |
This theorem depends on definitions: df-bi 110 df-nf 1350 |
This theorem is referenced by: nf3and 1461 nfbid 1480 nfsbxy 1818 nfsbxyt 1819 nfeud 1916 nfmod 1917 nfeqd 2192 nfeld 2193 nfabd 2196 nfned 2298 nfneld 2305 nfraldxy 2356 nfrexdxy 2357 nfraldya 2358 nfrexdya 2359 nfsbc1d 2780 nfsbcd 2783 nfbrd 3807 |
Copyright terms: Public domain | W3C validator |