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 1852	1 ⊢ (𝜑 → Ⅎ𝑥(𝜓 ∧ 𝜒))

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

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-ex 1778  df-nf 1782

This theorem is referenced by:  nf3and  1897  nfan  1898  nfbid  1901  nfeud2  2593  nfeudw  2594  nfeld  2920  nfreuwOLD  3433  nfrmowOLD  3434  nfrmod  3439  nfreud  3440  nfrmo  3441  nfrabwOLD  3484  nfrab  3486  nfifd  4577  nfdisjw  5145  nfdisj  5146  nfopabd  5234  dfid3  5596  nfriotadw  7412  nfriotad  7416  axrepndlem1  10661  axrepndlem2  10662  axunndlem1  10664  axunnd  10665  axregndlem2  10672  axinfndlem1  10674  axinfnd  10675  axacndlem4  10679  axacndlem5  10680  axacnd  10681  axsepg2  35058  axsepg2ALT  35059  bj-gabima  36906  cbvreud  37339  riotasv2d  38913