![]() |
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 1450 | . 2 ⊢ (Ⅎ𝑥𝜑 ↔ Ⅎ𝑥𝜓) |
4 | 1, 3 | sylibr 133 | 1 ⊢ (𝜒 → Ⅎ𝑥𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 Ⅎwnf 1437 |
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 1424 ax-gen 1426 |
This theorem depends on definitions: df-bi 116 df-nf 1438 |
This theorem is referenced by: nf3and 1549 nfbid 1568 nfsbxy 1916 nfsbxyt 1917 nfeud 2016 nfmod 2017 nfeqd 2297 nfeld 2298 nfabd 2301 nfned 2403 nfneld 2412 nfraldxy 2470 nfrexdxy 2471 nfraldya 2472 nfrexdya 2473 nfsbc1d 2929 nfsbcd 2932 nfbrd 3981 |
Copyright terms: Public domain | W3C validator |