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 1576 | . 2 ⊢ (⊤ → Ⅎ𝑥(𝜑 ↔ 𝜓)) |
6 | 5 | mptru 1352 | 1 ⊢ Ⅎ𝑥(𝜑 ↔ 𝜓) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 ⊤wtru 1344 Ⅎwnf 1448 |
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 1435 ax-gen 1437 ax-4 1498 ax-ial 1522 ax-i5r 1523 |
This theorem depends on definitions: df-bi 116 df-tru 1346 df-nf 1449 |
This theorem is referenced by: sb8eu 2027 nfeuv 2032 bm1.1 2150 abbi 2280 nfeq 2316 cleqf 2333 sbhypf 2775 ceqsexg 2854 elabgt 2867 elabgf 2868 copsex2t 4223 copsex2g 4224 opelopabsb 4238 opeliunxp2 4744 ralxpf 4750 rexxpf 4751 cbviota 5158 sb8iota 5160 fmptco 5651 nfiso 5774 dfoprab4f 6161 opeliunxp2f 6206 xpf1o 6810 bdsepnfALT 13771 |
Copyright terms: Public domain | W3C validator |