Theorem nfand 1896

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395  Ⅎwnf 1782

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1779  df-nf 1783

This theorem is referenced by:  nf3and  1897  nfan  1898  nfbid  1901  nfeud2  2588  nfeudw  2589  nfeld  2909  nfreuwOLD  3409  nfrmowOLD  3410  nfrmod  3415  nfreud  3416  nfrmo  3417  nfrabwOLD  3459  nfrab  3461  nfifd  4535  nfdisjw  5102  nfdisj  5103  nfopabd  5191  dfid3  5561  nfriotadw  7378  nfriotad  7381  axrepndlem1  10614  axrepndlem2  10615  axunndlem1  10617  axunnd  10618  axregndlem2  10625  axinfndlem1  10627  axinfnd  10628  axacndlem4  10632  axacndlem5  10633  axacnd  10634  axsepg2  35071  axsepg2ALT  35072  bj-gabima  36916  cbvreud  37349  riotasv2d  38933