Theorem nfand 1904

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396  Ⅎwnf 1790

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-ex 1787  df-nf 1791

This theorem is referenced by:  nf3and  1905  nfan  1906  nfbid  1909  nfeud2  2594  nfeudw  2595  nfeld  2913  nfrmod  3388  nfreud  3389  nfrmo  3390  nfrab  3430  nfifd  4491  nfdisjw  5058  nfdisj  5059  nfopabd  5147  dfid3  5523  nfriotadw  7328  nfriotad  7331  axrepndlem1  10513  axrepndlem2  10514  axunndlem1  10516  axunnd  10517  axregndlem2  10524  axinfndlem1  10526  axinfnd  10527  axacndlem4  10531  axacndlem5  10532  axacnd  10533  nfchnd  18575  axsepg2  35328  axsepg3  35329  axsepg3ALT  35330  axsepg5  35332  axtcond  36713  bj-gabima  37300  cbvreud  37742  riotasv2d  39456