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 1857 | . . 3 ⊢ Ⅎ𝑥 ¬ 𝜑 |
4 | nf.2 | . . 3 ⊢ Ⅎ𝑥𝜓 | |
5 | 3, 4 | nfim 1897 | . 2 ⊢ Ⅎ𝑥(¬ 𝜑 → 𝜓) |
6 | 1, 5 | nfxfr 1853 | 1 ⊢ Ⅎ𝑥(𝜑 ∨ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 843 Ⅎwnf 1784 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-ex 1781 df-nf 1785 |
This theorem is referenced by: nf3or 1906 axi12 2791 axbnd 2792 nfun 4141 nfpr 4628 rabsnifsb 4658 disjxun 5064 fsuppmapnn0fiubex 13361 nfsum1 15046 nfsumw 15047 nfsum 15048 nfcprod1 15264 nfcprod 15265 fdc1 35036 dvdsrabdioph 39427 disjinfi 41474 iundjiun 42762 |
Copyright terms: Public domain | W3C validator |