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 399 | . 2 ⊢ ((𝜓 ∧ 𝜒) ↔ ¬ (𝜓 → ¬ 𝜒)) | |
2 | nfand.1 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
3 | nfand.2 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜒) | |
4 | 3 | nfnd 1854 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜒) |
5 | 2, 4 | nfimd 1891 | . . 3 ⊢ (𝜑 → Ⅎ𝑥(𝜓 → ¬ 𝜒)) |
6 | 5 | nfnd 1854 | . 2 ⊢ (𝜑 → Ⅎ𝑥 ¬ (𝜓 → ¬ 𝜒)) |
7 | 1, 6 | nfxfrd 1850 | 1 ⊢ (𝜑 → Ⅎ𝑥(𝜓 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 398 Ⅎwnf 1780 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-ex 1777 df-nf 1781 |
This theorem is referenced by: nf3and 1895 nfan 1896 nfbid 1899 nfeud2 2672 nfeudw 2673 nfeld 2989 nfreud 3372 nfrmod 3373 nfreuw 3374 nfrmow 3375 nfrmo 3377 nfrabw 3385 nfrab 3386 nfifd 4494 nfdisjw 5035 nfdisj 5036 dfid3 5456 nfriotadw 7116 nfriotad 7119 axrepndlem1 10008 axrepndlem2 10009 axunndlem1 10011 axunnd 10012 axregndlem2 10019 axinfndlem1 10021 axinfnd 10022 axacndlem4 10026 axacndlem5 10027 axacnd 10028 cbvreud 34648 riotasv2d 36087 |
Copyright terms: Public domain | W3C validator |