Theorem nfand 1927

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400  Ⅎwnf 1813

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1810  df-nf 1814

This theorem is referenced by:  nf3and  1928  nfan  1929  nfbid  1932  nfeud2  2618  nfeudw  2619  nfeld  2936  nfrmod  3412  nfreud  3413  nfrmo  3414  nfrab  3453  nfifd  4518  nfdisjw  5089  nfdisj  5090  nfopabd  5180  dfid3  5561  nfriotadw  7377  nfriotad  7380  axrepndlem1  10578  axrepndlem2  10579  axunndlem1  10581  axunnd  10582  axregndlem2  10589  axinfndlem1  10591  axinfnd  10592  axacndlem4  10596  axacndlem5  10597  axacnd  10598  nfchnd  18668  axsepg2  35534  axsepg3  35535  axsepg3ALT  35536  axsepg5  35538  axtcond  36970  bj-gabima  37557  cbvreud  38000  riotasv2d  39712