![]() |
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 396 | . 2 ⊢ ((𝜓 ∧ 𝜒) ↔ ¬ (𝜓 → ¬ 𝜒)) | |
2 | nfand.1 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥𝜓) | |
3 | nfand.2 | . . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜒) | |
4 | 3 | nfnd 1856 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜒) |
5 | 2, 4 | nfimd 1892 | . . 3 ⊢ (𝜑 → Ⅎ𝑥(𝜓 → ¬ 𝜒)) |
6 | 5 | nfnd 1856 | . 2 ⊢ (𝜑 → Ⅎ𝑥 ¬ (𝜓 → ¬ 𝜒)) |
7 | 1, 6 | nfxfrd 1851 | 1 ⊢ (𝜑 → Ⅎ𝑥(𝜓 ∧ 𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 Ⅎ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 207 df-an 396 df-or 848 df-ex 1777 df-nf 1781 |
This theorem is referenced by: nf3and 1896 nfan 1897 nfbid 1900 nfeud2 2588 nfeudw 2589 nfeld 2915 nfreuwOLD 3423 nfrmowOLD 3424 nfrmod 3429 nfreud 3430 nfrmo 3431 nfrabwOLD 3474 nfrab 3476 nfifd 4560 nfdisjw 5127 nfdisj 5128 nfopabd 5216 dfid3 5586 nfriotadw 7396 nfriotad 7399 axrepndlem1 10630 axrepndlem2 10631 axunndlem1 10633 axunnd 10634 axregndlem2 10641 axinfndlem1 10643 axinfnd 10644 axacndlem4 10648 axacndlem5 10649 axacnd 10650 axsepg2 35075 axsepg2ALT 35076 bj-gabima 36923 cbvreud 37356 riotasv2d 38939 |
Copyright terms: Public domain | W3C validator |