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 1434 | . 2 ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓) |
4 | 1, 3 | sylibr 133 | 1 ⊢ (𝜒 → Ⅎ𝑥𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 Ⅎwnf 1421 |
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 df-nf 1422 |
This theorem is referenced by: nf3and 1533 nfbid 1552 nfsbxy 1895 nfsbxyt 1896 nfeud 1993 nfmod 1994 nfeqd 2273 nfeld 2274 nfabd 2277 nfned 2379 nfneld 2388 nfraldxy 2444 nfrexdxy 2445 nfraldya 2446 nfrexdya 2447 nfsbc1d 2898 nfsbcd 2901 nfbrd 3943 |
Copyright terms: Public domain | W3C validator |