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 1581 | . 2 ⊢ (⊤ → Ⅎ𝑥(𝜑 ↔ 𝜓)) |
6 | 5 | mptru 1357 | 1 ⊢ Ⅎ𝑥(𝜑 ↔ 𝜓) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ⊤wtru 1349 Ⅎwnf 1453 |
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 1440 ax-gen 1442 ax-4 1503 ax-ial 1527 ax-i5r 1528 |
This theorem depends on definitions: df-bi 116 df-tru 1351 df-nf 1454 |
This theorem is referenced by: sb8eu 2032 nfeuv 2037 bm1.1 2155 abbi 2284 nfeq 2320 cleqf 2337 sbhypf 2779 ceqsexg 2858 elabgt 2871 elabgf 2872 copsex2t 4230 copsex2g 4231 opelopabsb 4245 opeliunxp2 4751 ralxpf 4757 rexxpf 4758 cbviota 5165 sb8iota 5167 fmptco 5662 nfiso 5785 dfoprab4f 6172 opeliunxp2f 6217 xpf1o 6822 bdsepnfALT 13924 |
Copyright terms: Public domain | W3C validator |