|   | 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 1857 | . . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜒) | 
| 5 | 2, 4 | nfimd 1893 | . . 3 ⊢ (𝜑 → Ⅎ𝑥(𝜓 → ¬ 𝜒)) | 
| 6 | 5 | nfnd 1857 | . 2 ⊢ (𝜑 → Ⅎ𝑥 ¬ (𝜓 → ¬ 𝜒)) | 
| 7 | 1, 6 | nfxfrd 1853 | 1 ⊢ (𝜑 → Ⅎ𝑥(𝜓 ∧ 𝜒)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 Ⅎwnf 1782 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-ex 1779 df-nf 1783 | 
| This theorem is referenced by: nf3and 1897 nfan 1898 nfbid 1901 nfeud2 2589 nfeudw 2590 nfeld 2916 nfreuwOLD 3425 nfrmowOLD 3426 nfrmod 3431 nfreud 3432 nfrmo 3433 nfrabwOLD 3475 nfrab 3477 nfifd 4554 nfdisjw 5121 nfdisj 5122 nfopabd 5210 dfid3 5580 nfriotadw 7397 nfriotad 7400 axrepndlem1 10633 axrepndlem2 10634 axunndlem1 10636 axunnd 10637 axregndlem2 10644 axinfndlem1 10646 axinfnd 10647 axacndlem4 10651 axacndlem5 10652 axacnd 10653 axsepg2 35097 axsepg2ALT 35098 bj-gabima 36942 cbvreud 37375 riotasv2d 38959 | 
| Copyright terms: Public domain | W3C validator |