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 1908 | . 2 ⊢ (⊤ → Ⅎ𝑥(𝜑 ↔ 𝜓)) |
6 | 5 | mptru 1549 | 1 ⊢ Ⅎ𝑥(𝜑 ↔ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ⊤wtru 1543 Ⅎwnf 1790 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-tru 1545 df-ex 1787 df-nf 1791 |
This theorem is referenced by: sbbib 2361 euf 2577 sb8eulem 2599 axextmo 2714 abbi 2805 cleqh 2856 cleqf 2930 sbhypf 3455 ceqsexg 3547 elabgt 3565 elabgf 3566 elabg 3570 axrep1 5152 axrep3 5155 axrep4 5156 copsex2t 5346 copsex2gOLD 5348 opeliunxp2 5675 ralxpf 5683 cbviotaw 6298 cbviota 6301 sb8iota 6303 fvopab5 6801 fmptco 6895 nfiso 7082 dfoprab4f 7772 opeliunxp2f 7898 xpf1o 8722 zfcndrep 10107 gsumcom2 19207 isfildlem 22601 cnextfvval 22809 mbfsup 24409 mbfinf 24410 brabgaf 30514 fmptcof2 30561 bnj1468 32389 subtr2 34134 mpobi123f 35932 eqrelf 36007 fourierdlem31 43205 |
Copyright terms: Public domain | W3C validator |