Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nfor | Structured version Visualization version GIF version |
Description: If 𝑥 is not free in 𝜑 and 𝜓, then it is not free in (𝜑 ∨ 𝜓). (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nf.1 | ⊢ Ⅎ𝑥𝜑 |
nf.2 | ⊢ Ⅎ𝑥𝜓 |
Ref | Expression |
---|---|
nfor | ⊢ Ⅎ𝑥(𝜑 ∨ 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-or 844 | . 2 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓)) | |
2 | nf.1 | . . . 4 ⊢ Ⅎ𝑥𝜑 | |
3 | 2 | nfn 1853 | . . 3 ⊢ Ⅎ𝑥 ¬ 𝜑 |
4 | nf.2 | . . 3 ⊢ Ⅎ𝑥𝜓 | |
5 | 3, 4 | nfim 1893 | . 2 ⊢ Ⅎ𝑥(¬ 𝜑 → 𝜓) |
6 | 1, 5 | nfxfr 1849 | 1 ⊢ Ⅎ𝑥(𝜑 ∨ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 843 Ⅎwnf 1780 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-ex 1777 df-nf 1781 |
This theorem is referenced by: nf3or 1902 axi12 2789 axi12OLD 2790 axbnd 2791 nfun 4141 nfpr 4622 rabsnifsb 4652 disjxun 5057 fsuppmapnn0fiubex 13354 nfsum1 15040 nfsumw 15041 nfsum 15042 nfcprod1 15258 nfcprod 15259 fdc1 35015 dvdsrabdioph 39400 disjinfi 41446 iundjiun 42735 |
Copyright terms: Public domain | W3C validator |