Theorem nfand 1997

Description: If in a context 𝑥 is not free in 𝜓 and 𝜒, then it is not free in (𝜓 ∧ 𝜒). (Contributed by Mario Carneiro, 7-Oct-2016.)

Hypotheses

Ref	Expression
nfand.1	⊢ (𝜑 → Ⅎ𝑥𝜓)
nfand.2	⊢ (𝜑 → Ⅎ𝑥𝜒)

Assertion

Ref	Expression
nfand	⊢ (𝜑 → Ⅎ𝑥(𝜓 ∧ 𝜒))

Proof of Theorem nfand

Step	Hyp	Ref	Expression
1		df-an 386	. 2 ⊢ ((𝜓 ∧ 𝜒) ↔ ¬ (𝜓 → ¬ 𝜒))
2		nfand.1	. . . 4 ⊢ (𝜑 → Ⅎ𝑥𝜓)
3		nfand.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜒)
4	3	nfnd 1955	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜒)
5	2, 4	nfimd 1993	. . 3 ⊢ (𝜑 → Ⅎ𝑥(𝜓 → ¬ 𝜒))
6	5	nfnd 1955	. 2 ⊢ (𝜑 → Ⅎ𝑥 ¬ (𝜓 → ¬ 𝜒))
7	1, 6	nfxfrd 1950	1 ⊢ (𝜑 → Ⅎ𝑥(𝜓 ∧ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 385  Ⅎwnf 1879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-ex 1876  df-nf 1880

This theorem is referenced by:  nf3and  1998  nfan  1999  nfbid  2002  nfeud2  2630  nfeld  2950  nfreud  3293  nfrmod  3294  nfrmo  3296  nfrab  3305  nfifd  4305  nfdisj  4823  dfid3  5221  nfriotad  6847  axrepndlem1  9702  axrepndlem2  9703  axunndlem1  9705  axunnd  9706  axregndlem2  9713  axinfndlem1  9715  axinfnd  9716  axacndlem4  9720  axacndlem5  9721  axacnd  9722  riotasv2d  34978