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 4228 copsex2g 4229 opelopabsb 4243 opeliunxp2 4749 ralxpf 4755 rexxpf 4756 cbviota 5163 sb8iota 5165 fmptco 5659 nfiso 5782 dfoprab4f 6169 opeliunxp2f 6214 xpf1o 6818 bdsepnfALT 13884 |
Copyright terms: Public domain | W3C validator |