Theorem nfand 1920

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400  Ⅎwnf 1806

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1803  df-nf 1807

This theorem is referenced by:  nf3and  1921  nfan  1922  nfbid  1925  nfeud2  2620  nfeudw  2621  nfeld  2938  nfrmod  3413  nfreud  3414  nfrmo  3415  nfrab  3455  nfifd  4513  nfdisjw  5084  nfdisj  5085  nfopabd  5173  dfid3  5550  nfriotadw  7365  nfriotad  7368  axrepndlem1  10565  axrepndlem2  10566  axunndlem1  10568  axunnd  10569  axregndlem2  10576  axinfndlem1  10578  axinfnd  10579  axacndlem4  10583  axacndlem5  10584  axacnd  10585  nfchnd  18657  axsepg2  35448  axsepg3  35449  axsepg3ALT  35450  axsepg5  35452  axtcond  36851  bj-gabima  37437  cbvreud  37879  riotasv2d  39593