Theorem nfand 1929

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

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

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

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

This theorem is used by:  nf3and  1930  nfan  1931  nfbid  1934  nfeud2  2615  nfeudw  2616  nfeld  2933  nfrmod  3408  nfreud  3409  nfrmo  3410  nfrab  3448  nfifd  4511  nfdisjw  5081  nfdisj  5082  nfopabd  5172  dfid3  5548  nfriotadw  7386  nfriotad  7389  axrepndlem1  10681  axrepndlem2  10682  axunndlem1  10684  axunnd  10685  axregndlem2  10692  axinfndlem1  10694  axinfnd  10695  axacndlem4  10699  axacndlem5  10700  axacnd  10701  nfchnd  18791  axsepg2  35865  axsepg3  35866  axsepg3ALT  35867  axsepg5  35869  axtcond  37359  bj-gabima  37946  cbvreud  38390  riotasv2d  40108