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 1567 | . 2 ⊢ (⊤ → Ⅎ𝑥(𝜑 ↔ 𝜓)) |
6 | 5 | mptru 1340 | 1 ⊢ Ⅎ𝑥(𝜑 ↔ 𝜓) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ⊤wtru 1332 Ⅎwnf 1436 |
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 1423 ax-gen 1425 ax-4 1487 ax-ial 1514 ax-i5r 1515 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 |
This theorem is referenced by: sb8eu 2012 nfeuv 2017 bm1.1 2124 abbi 2253 nfeq 2289 cleqf 2305 sbhypf 2735 ceqsexg 2813 elabgt 2825 elabgf 2826 copsex2t 4167 copsex2g 4168 opelopabsb 4182 opeliunxp2 4679 ralxpf 4685 rexxpf 4686 cbviota 5093 sb8iota 5095 fmptco 5586 nfiso 5707 dfoprab4f 6091 opeliunxp2f 6135 xpf1o 6738 bdsepnfALT 13087 strcollnfALT 13184 |
Copyright terms: Public domain | W3C validator |