![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfbi | Structured version Visualization version GIF version |
Description: If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑 ↔ 𝜓). (Contributed by NM, 26-May-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) |
Ref | Expression |
---|---|
nf.1 | ⊢ Ⅎ𝑥𝜑 |
nf.2 | ⊢ Ⅎ𝑥𝜓 |
Ref | Expression |
---|---|
nfbi | ⊢ Ⅎ𝑥(𝜑 ↔ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nf.1 | . . . 4 ⊢ Ⅎ𝑥𝜑 | |
2 | 1 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝜑) |
3 | nf.2 | . . . 4 ⊢ Ⅎ𝑥𝜓 | |
4 | 3 | a1i 11 | . . 3 ⊢ (⊤ → Ⅎ𝑥𝜓) |
5 | 2, 4 | nfbid 1969 | . 2 ⊢ (⊤ → Ⅎ𝑥(𝜑 ↔ 𝜓)) |
6 | 5 | trud 1630 | 1 ⊢ Ⅎ𝑥(𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ⊤wtru 1621 Ⅎwnf 1845 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1623 df-ex 1842 df-nf 1847 |
This theorem is referenced by: euf 2603 sb8eu 2629 bm1.1 2733 cleqh 2850 sbhypf 3381 ceqsexg 3461 elabgt 3475 elabgf 3476 axrep1 4912 axrep3 4914 axrep4 4915 copsex2t 5093 copsex2g 5094 opelopabsb 5123 opeliunxp2 5404 ralxpf 5412 cbviota 6005 sb8iota 6007 fvopab5 6460 fmptco 6547 nfiso 6723 dfoprab4f 7381 opeliunxp2f 7493 xpf1o 8275 zfcndrep 9599 gsumcom2 18545 isfildlem 21833 cnextfvval 22041 mbfsup 23601 mbfinf 23602 brabgaf 29698 fmptcof2 29737 bnj1468 31194 subtr2 32586 bj-abbi 33052 bj-axrep1 33065 bj-axrep3 33067 bj-axrep4 33068 mpt2bi123f 34253 eqrelf 34313 fourierdlem31 40827 |
Copyright terms: Public domain | W3C validator |