Theorem nfand 1900

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396  Ⅎwnf 1786

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-nf 1787

This theorem is referenced by:  nf3and  1901  nfan  1902  nfbid  1905  nfeud2  2590  nfeudw  2591  nfeld  2918  nfreud  3302  nfrmod  3303  nfreuwOLD  3306  nfrmowOLD  3307  nfrmo  3309  nfrabwOLD  3319  nfrab  3320  nfifd  4488  nfdisjw  5051  nfdisj  5052  nfopabd  5142  dfid3  5492  nfriotadw  7240  nfriotad  7244  axrepndlem1  10348  axrepndlem2  10349  axunndlem1  10351  axunnd  10352  axregndlem2  10359  axinfndlem1  10361  axinfnd  10362  axacndlem4  10366  axacndlem5  10367  axacnd  10368  bj-gabima  35128  cbvreud  35544  riotasv2d  36971