Theorem nfand 1932

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 1929	. . 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  1933  nfan  1934  nfbid  1937  nfeud2  2618  nfeudw  2619  nfeld  2937  nfrmod  3412  nfreud  3413  nfrmo  3414  nfrab  3452  nfifd  4515  nfdisjw  5085  nfdisj  5086  nfopabd  5177  dfid3  5554  nfriotadw  7411  nfriotad  7414  axrepndlem1  10707  axrepndlem2  10708  axunndlem1  10710  axunnd  10711  axregndlem2  10718  axinfndlem1  10720  axinfnd  10721  axacndlem4  10725  axacndlem5  10726  axacnd  10727  nfchnd  18817  axsepg2  35921  axsepg3  35922  axsepg3ALT  35923  axsepg5  35925  axtcond  37457  bj-gabima  38044  cbvreud  38501  riotasv2d  40217