![]() |
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 1872 | . 2 ⊢ (⊤ → Ⅎ𝑥(𝜑 ↔ 𝜓)) |
6 | 5 | trud 1533 | 1 ⊢ Ⅎ𝑥(𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ⊤wtru 1524 Ⅎwnf 1748 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 |
This theorem is referenced by: euf 2506 sb8eu 2532 bm1.1 2636 cleqh 2753 sbhypf 3284 ceqsexg 3365 elabgt 3379 elabgf 3380 axrep1 4805 axrep3 4807 axrep4 4808 copsex2t 4986 copsex2g 4987 opelopabsb 5014 opeliunxp2 5293 ralxpf 5301 cbviota 5894 sb8iota 5896 fvopab5 6349 fmptco 6436 nfiso 6612 dfoprab4f 7270 opeliunxp2f 7381 xpf1o 8163 zfcndrep 9474 gsumcom2 18420 isfildlem 21708 cnextfvval 21916 mbfsup 23476 mbfinf 23477 brabgaf 29546 fmptcof2 29585 bnj1468 31042 subtr2 32434 bj-abbi 32900 bj-axrep1 32913 bj-axrep3 32915 bj-axrep4 32916 mpt2bi123f 34101 eqrelf 34161 fourierdlem31 40673 |
Copyright terms: Public domain | W3C validator |