Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nfand | Structured version Visualization version GIF version |
Description: If in a context 𝑥 is not free in 𝜓 and 𝜒, it is not free in (𝜓 ∧ 𝜒). (Contributed by Mario Carneiro, 7-Oct-2016.) |
Ref | Expression |
---|---|
nfand.1 | ⊢ (𝜑 → Ⅎ𝑥𝜓) |
nfand.2 | ⊢ (𝜑 → Ⅎ𝑥𝜒) |
Ref | Expression |
---|---|
nfand | ⊢ (𝜑 → Ⅎ𝑥(𝜓 ∧ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-an 385 | . 2 ⊢ ((𝜓 ∧ 𝜒) ↔ ¬ (𝜓 → ¬ 𝜒)) | |
2 | nfand.1 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
3 | nfand.2 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜒) | |
4 | 3 | nfnd 1769 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜒) |
5 | 2, 4 | nfimd 1812 | . . 3 ⊢ (𝜑 → Ⅎ𝑥(𝜓 → ¬ 𝜒)) |
6 | 5 | nfnd 1769 | . 2 ⊢ (𝜑 → Ⅎ𝑥 ¬ (𝜓 → ¬ 𝜒)) |
7 | 1, 6 | nfxfrd 1772 | 1 ⊢ (𝜑 → Ⅎ𝑥(𝜓 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 383 Ⅎwnf 1699 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-ex 1696 df-nf 1701 |
This theorem is referenced by: nf3and 1815 nfan 1816 nfbid 1820 nfeld 2759 nfreud 3091 nfrmod 3092 nfrmo 3094 nfrab 3100 nfifd 4064 nfdisj 4565 dfid3 4954 nfriotad 6519 axrepndlem1 9293 axrepndlem2 9294 axunndlem1 9296 axunnd 9297 axregndlem2 9304 axinfndlem1 9306 axinfnd 9307 axacndlem4 9311 axacndlem5 9312 axacnd 9313 riotasv2d 33261 |
Copyright terms: Public domain | W3C validator |