Theorem nfand 1896

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 1857	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜒)
5	2, 4	nfimd 1893	. . 3 ⊢ (𝜑 → Ⅎ𝑥(𝜓 → ¬ 𝜒))
6	5	nfnd 1857	. 2 ⊢ (𝜑 → Ⅎ𝑥 ¬ (𝜓 → ¬ 𝜒))
7	1, 6	nfxfrd 1853	1 ⊢ (𝜑 → Ⅎ𝑥(𝜓 ∧ 𝜒))

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