New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > nfbi | GIF version |
Description: If x is not free in φ and ψ, it is not free in (φ ↔ ψ). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) |
Ref | Expression |
---|---|
nf.1 | ⊢ Ⅎxφ |
nf.2 | ⊢ Ⅎxψ |
Ref | Expression |
---|---|
nfbi | ⊢ Ⅎx(φ ↔ ψ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nf.1 | . . . 4 ⊢ Ⅎxφ | |
2 | 1 | a1i 10 | . . 3 ⊢ ( ⊤ → Ⅎxφ) |
3 | nf.2 | . . . 4 ⊢ Ⅎxψ | |
4 | 3 | a1i 10 | . . 3 ⊢ ( ⊤ → Ⅎxψ) |
5 | 2, 4 | nfbid 1832 | . 2 ⊢ ( ⊤ → Ⅎx(φ ↔ ψ)) |
6 | 5 | trud 1323 | 1 ⊢ Ⅎx(φ ↔ ψ) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 176 ⊤ wtru 1316 Ⅎwnf 1544 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-11 1746 |
This theorem depends on definitions: df-bi 177 df-an 360 df-tru 1319 df-ex 1542 df-nf 1545 |
This theorem is referenced by: euf 2210 sb8eu 2222 bm1.1 2338 abbi 2463 nfeq 2496 cleqf 2513 sbhypf 2904 ceqsexg 2970 elabgt 2982 elabgf 2983 cbviota 4344 sb8iota 4346 copsex2t 4608 copsex2g 4609 opelopabsb 4697 opeliunxp2 4822 ralxpf 4827 nfiso 5487 |
Copyright terms: Public domain | W3C validator |