Theorem nfand 1893

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 1854	. . . 4 ⊢ (𝜑 → Ⅎ𝑥 ¬ 𝜒)
5	2, 4	nfimd 1890	. . 3 ⊢ (𝜑 → Ⅎ𝑥(𝜓 → ¬ 𝜒))
6	5	nfnd 1854	. 2 ⊢ (𝜑 → Ⅎ𝑥 ¬ (𝜓 → ¬ 𝜒))
7	1, 6	nfxfrd 1849	1 ⊢ (𝜑 → Ⅎ𝑥(𝜓 ∧ 𝜒))

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

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-ex 1775  df-nf 1779

This theorem is referenced by:  nf3and  1894  nfan  1895  nfbid  1898  nfeud2  2580  nfeudw  2581  nfeld  2910  nfreuwOLD  3418  nfrmowOLD  3419  nfrmod  3424  nfreud  3425  nfrmo  3426  nfrabwOLD  3465  nfrab  3468  nfifd  4553  nfdisjw  5119  nfdisj  5120  nfopabd  5210  dfid3  5573  nfriotadw  7378  nfriotad  7382  axrepndlem1  10609  axrepndlem2  10610  axunndlem1  10612  axunnd  10613  axregndlem2  10620  axinfndlem1  10622  axinfnd  10623  axacndlem4  10627  axacndlem5  10628  axacnd  10629  bj-gabima  36412  cbvreud  36846  riotasv2d  38423