Theorem nfand 1898

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 396	. 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 ⊢ (𝜑 → Ⅎ𝑥(𝜓 ∧ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395  Ⅎwnf 1784

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1781  df-nf 1785

This theorem is referenced by:  nf3and  1899  nfan  1900  nfbid  1903  nfeud2  2587  nfeudw  2588  nfeld  2907  nfrmod  3392  nfreud  3393  nfrmo  3394  nfrab  3435  nfifd  4504  nfdisjw  5072  nfdisj  5073  nfopabd  5161  dfid3  5517  nfriotadw  7317  nfriotad  7320  axrepndlem1  10490  axrepndlem2  10491  axunndlem1  10493  axunnd  10494  axregndlem2  10501  axinfndlem1  10503  axinfnd  10504  axacndlem4  10508  axacndlem5  10509  axacnd  10510  nfchnd  18519  axsepg2  35115  axsepg2ALT  35116  bj-gabima  37005  cbvreud  37438  riotasv2d  39077