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 𝜓, then 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 1905 | . 2 ⊢ (⊤ → Ⅎ𝑥(𝜑 ↔ 𝜓)) |
6 | 5 | mptru 1546 | 1 ⊢ Ⅎ𝑥(𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ⊤wtru 1540 Ⅎwnf 1786 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-tru 1542 df-ex 1783 df-nf 1787 |
This theorem is referenced by: sbbib 2359 euf 2576 sb8eulem 2598 axextmo 2713 abbi 2810 cleqh 2862 cleqf 2938 sbhypf 3491 ceqsexg 3583 elabgtOLD 3604 elabgf 3605 elabgOLD 3608 axrep1 5210 axrep3 5213 axrep4 5214 copsex2t 5406 copsex2gOLD 5408 opeliunxp2 5747 ralxpf 5755 cbviotaw 6398 cbviota 6401 sb8iota 6403 fvopab5 6907 fmptco 7001 nfiso 7193 dfoprab4f 7896 opeliunxp2f 8026 xpf1o 8926 zfcndrep 10370 gsumcom2 19576 isfildlem 23008 cnextfvval 23216 mbfsup 24828 mbfinf 24829 brabgaf 30948 fmptcof2 30994 bnj1468 32826 subtr2 34504 mpobi123f 36320 eqrelf 36395 fourierdlem31 43679 |
Copyright terms: Public domain | W3C validator |