| 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 849 | . 2 ⊢ ((𝜑 ∨ 𝜓) ↔ (¬ 𝜑 → 𝜓)) | |
| 2 | nf.1 | . . . 4 ⊢ Ⅎ𝑥𝜑 | |
| 3 | 2 | nfn 1857 | . . 3 ⊢ Ⅎ𝑥 ¬ 𝜑 |
| 4 | nf.2 | . . 3 ⊢ Ⅎ𝑥𝜓 | |
| 5 | 3, 4 | nfim 1896 | . 2 ⊢ Ⅎ𝑥(¬ 𝜑 → 𝜓) |
| 6 | 1, 5 | nfxfr 1853 | 1 ⊢ Ⅎ𝑥(𝜑 ∨ 𝜓) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ∨ wo 848 Ⅎ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-ex 1780 df-nf 1784 |
| This theorem is referenced by: nf3or 1905 axi12 2706 axbnd 2707 nfun 4170 nfunOLD 4171 nfpr 4692 rabsnifsb 4722 disjxun 5141 fsuppmapnn0fiubex 14033 nfsum1 15726 nfsum 15727 nfcprod1 15944 nfcprod 15945 fdc1 37753 dvdsrabdioph 42821 mnringmulrcld 44247 disjinfi 45197 iundjiun 46475 |
| Copyright terms: Public domain | W3C validator |