Theorem nfand 1900

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 397	. 2 ⊢ ((𝜓 ∧ 𝜒) ↔ ¬ (𝜓 → ¬ 𝜒))
2		nfand.1	. . . 4 ⊢ (𝜑 → Ⅎ𝑥𝜓)
3		nfand.2	. . . . 5 ⊢ (𝜑 → Ⅎ𝑥𝜒)
4	3	nfnd 1861	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜒)
5	2, 4	nfimd 1897	. . 3 ⊢ (𝜑 → Ⅎ𝑥(𝜓 → ¬ 𝜒))
6	5	nfnd 1861	. 2 ⊢ (𝜑 → Ⅎ𝑥 ¬ (𝜓 → ¬ 𝜒))
7	1, 6	nfxfrd 1856	1 ⊢ (𝜑 → Ⅎ𝑥(𝜓 ∧ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396  Ⅎwnf 1785

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-nf 1786

This theorem is referenced by:  nf3and  1901  nfan  1902  nfbid  1905  nfeud2  2584  nfeudw  2585  nfeld  2914  nfreuwOLD  3422  nfrmowOLD  3423  nfrmod  3428  nfreud  3429  nfrmo  3430  nfrabwOLD  3469  nfrab  3472  nfifd  4557  nfdisjw  5125  nfdisj  5126  nfopabd  5216  dfid3  5577  nfriotadw  7372  nfriotad  7376  axrepndlem1  10586  axrepndlem2  10587  axunndlem1  10589  axunnd  10590  axregndlem2  10597  axinfndlem1  10599  axinfnd  10600  axacndlem4  10604  axacndlem5  10605  axacnd  10606  bj-gabima  35815  cbvreud  36249  riotasv2d  37822