![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfbi | GIF version |
Description: If 𝑥 is not free in 𝜑 and 𝜓, then it is not free in (𝜑 ↔ 𝜓). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) |
Ref | Expression |
---|---|
nfbi.1 | ⊢ Ⅎ𝑥𝜑 |
nfbi.2 | ⊢ Ⅎ𝑥𝜓 |
Ref | Expression |
---|---|
nfbi | ⊢ Ⅎ𝑥(𝜑 ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfbi.1 | . . . 4 ⊢ Ⅎ𝑥𝜑 | |
2 | 1 | a1i 9 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝜑) |
3 | nfbi.2 | . . . 4 ⊢ Ⅎ𝑥𝜓 | |
4 | 3 | a1i 9 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝜓) |
5 | 2, 4 | nfbid 1588 | . 2 ⊢ (⊤ → Ⅎ𝑥(𝜑 ↔ 𝜓)) |
6 | 5 | mptru 1362 | 1 ⊢ Ⅎ𝑥(𝜑 ↔ 𝜓) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 ⊤wtru 1354 Ⅎwnf 1460 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-4 1510 ax-ial 1534 ax-i5r 1535 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 |
This theorem is referenced by: sb8eu 2039 nfeuv 2044 bm1.1 2162 abbi 2291 nfeq 2327 cleqf 2344 sbhypf 2786 ceqsexg 2865 elabgt 2878 elabgf 2879 copsex2t 4245 copsex2g 4246 opelopabsb 4260 opeliunxp2 4767 ralxpf 4773 rexxpf 4774 cbviota 5183 sb8iota 5185 fmptco 5682 nfiso 5806 dfoprab4f 6193 opeliunxp2f 6238 xpf1o 6843 bdsepnfALT 14611 |
Copyright terms: Public domain | W3C validator |