Theorem nfand 1930

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817

This theorem is used by:  nf3and  1931  nfan  1932  nfbid  1935  nfeud2  2616  nfeudw  2617  nfeld  2934  nfrmod  3409  nfreud  3410  nfrmo  3411  nfrab  3449  nfifd  4512  nfdisjw  5082  nfdisj  5083  nfopabd  5173  dfid3  5549  nfriotadw  7377  nfriotad  7380  axrepndlem1  10658  axrepndlem2  10659  axunndlem1  10661  axunnd  10662  axregndlem2  10669  axinfndlem1  10671  axinfnd  10672  axacndlem4  10676  axacndlem5  10677  axacnd  10678  nfchnd  18765  axsepg2  35781  axsepg3  35782  axsepg3ALT  35783  axsepg5  35785  axtcond  37236  bj-gabima  37823  cbvreud  38264  riotasv2d  39982