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  2621  nfeudw  2622  nfeld  2939  nfrmod  3415  nfreud  3416  nfrmo  3417  nfrab  3456  nfifd  4522  nfdisjw  5093  nfdisj  5094  nfopabd  5184  dfid3  5564  nfriotadw  7388  nfriotad  7391  axrepndlem1  10595  axrepndlem2  10596  axunndlem1  10598  axunnd  10599  axregndlem2  10606  axinfndlem1  10608  axinfnd  10609  axacndlem4  10613  axacndlem5  10614  axacnd  10615  nfchnd  18692  axsepg2  35577  axsepg3  35578  axsepg3ALT  35579  axsepg5  35581  axtcond  37030  bj-gabima  37617  cbvreud  38060  riotasv2d  39772