Theorem nfand 1916

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399  Ⅎwnf 1802

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-ex 1799  df-nf 1803

This theorem is referenced by:  nf3and  1917  nfan  1918  nfbid  1921  nfeud2  2616  nfeudw  2617  nfeld  2934  nfrmod  3409  nfreud  3410  nfrmo  3411  nfrab  3451  nfifd  4509  nfdisjw  5078  nfdisj  5079  nfopabd  5167  dfid3  5543  nfriotadw  7357  nfriotad  7360  axrepndlem1  10547  axrepndlem2  10548  axunndlem1  10550  axunnd  10551  axregndlem2  10558  axinfndlem1  10560  axinfnd  10561  axacndlem4  10565  axacndlem5  10566  axacnd  10567  nfchnd  18626  axsepg2  35400  axsepg3  35401  axsepg3ALT  35402  axsepg5  35404  axtcond  36802  bj-gabima  37389  cbvreud  37831  riotasv2d  39545