Theorem nfand 1930

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817

This theorem is used by:  nf3and  1931  nfan  1932  nfbid  1935  nfeud2  2617  nfeudw  2618  nfeld  2935  nfrmod  3410  nfreud  3411  nfrmo  3412  nfrab  3451  nfifd  4515  nfdisjw  5086  nfdisj  5087  nfopabd  5177  dfid3  5557  nfriotadw  7382  nfriotad  7385  axrepndlem1  10605  axrepndlem2  10606  axunndlem1  10608  axunnd  10609  axregndlem2  10616  axinfndlem1  10618  axinfnd  10619  axacndlem4  10623  axacndlem5  10624  axacnd  10625  nfchnd  18705  axsepg2  35674  axsepg3  35675  axsepg3ALT  35676  axsepg5  35678  axtcond  37105  bj-gabima  37692  cbvreud  38135  riotasv2d  39838