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 848 | . 2 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓)) | |
2 | nf.1 | . . . 4 ⊢ Ⅎ𝑥𝜑 | |
3 | 2 | nfn 1865 | . . 3 ⊢ Ⅎ𝑥 ¬ 𝜑 |
4 | nf.2 | . . 3 ⊢ Ⅎ𝑥𝜓 | |
5 | 3, 4 | nfim 1904 | . 2 ⊢ Ⅎ𝑥(¬ 𝜑 → 𝜓) |
6 | 1, 5 | nfxfr 1860 | 1 ⊢ Ⅎ𝑥(𝜑 ∨ 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 847 Ⅎwnf 1791 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-ex 1788 df-nf 1792 |
This theorem is referenced by: nf3or 1913 axi12 2706 axbnd 2707 nfun 4065 nfpr 4592 rabsnifsb 4624 disjxun 5037 fsuppmapnn0fiubex 13530 nfsum1 15218 nfsum 15219 nfsumOLD 15220 nfcprod1 15435 nfcprod 15436 fdc1 35590 dvdsrabdioph 40276 mnringmulrcld 41460 disjinfi 42345 iundjiun 43616 |
Copyright terms: Public domain | W3C validator |