![]() |
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 𝜒, then 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 400 | . 2 ⊢ ((𝜓 ∧ 𝜒) ↔ ¬ (𝜓 → ¬ 𝜒)) | |
2 | nfand.1 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
3 | nfand.2 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜒) | |
4 | 3 | nfnd 1859 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜒) |
5 | 2, 4 | nfimd 1895 | . . 3 ⊢ (𝜑 → Ⅎ𝑥(𝜓 → ¬ 𝜒)) |
6 | 5 | nfnd 1859 | . 2 ⊢ (𝜑 → Ⅎ𝑥 ¬ (𝜓 → ¬ 𝜒)) |
7 | 1, 6 | nfxfrd 1855 | 1 ⊢ (𝜑 → Ⅎ𝑥(𝜓 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 399 Ⅎwnf 1785 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-ex 1782 df-nf 1786 |
This theorem is referenced by: nf3and 1899 nfan 1900 nfbid 1903 nfeud2 2651 nfeudw 2652 nfeld 2966 nfreud 3325 nfrmod 3326 nfreuw 3327 nfrmow 3328 nfrmo 3330 nfrabw 3338 nfrab 3339 nfifd 4453 nfdisjw 5007 nfdisj 5008 dfid3 5427 nfriotadw 7101 nfriotad 7104 axrepndlem1 10003 axrepndlem2 10004 axunndlem1 10006 axunnd 10007 axregndlem2 10014 axinfndlem1 10016 axinfnd 10017 axacndlem4 10021 axacndlem5 10022 axacnd 10023 cbvreud 34790 riotasv2d 36253 |
Copyright terms: Public domain | W3C validator |