| 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 1902 | . 2 ⊢ (⊤ → Ⅎ𝑥(𝜑 ↔ 𝜓)) |
| 6 | 5 | mptru 1547 | 1 ⊢ Ⅎ𝑥(𝜑 ↔ 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: ↔ wb 206 ⊤wtru 1541 Ⅎwnf 1783 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-nf 1784 |
| This theorem is referenced by: sbbib 2364 euf 2576 sb8eulem 2598 axextmo 2712 abbib 2811 cleqh 2871 cleqf 2934 sbhypfOLD 3545 ceqsexg 3653 elabgf 3674 axrep1 5280 axrep3 5283 axrep4OLD 5286 copsex2t 5497 opeliunxp2 5849 ralxpf 5857 cbviotaw 6521 cbviota 6523 sb8iota 6525 fvopab5 7049 fmptco 7149 nfiso 7342 dfoprab4f 8081 opeliunxp2f 8235 xpf1o 9179 zfcndrep 10654 gsumcom2 19993 isfildlem 23865 cnextfvval 24073 mbfsup 25699 mbfinf 25700 brabgaf 32620 fmptcof2 32667 bnj1468 34860 subtr2 36316 mpobi123f 38169 eqrelf 38256 unielss 43230 fourierdlem31 46153 |
| Copyright terms: Public domain | W3C validator |