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 1860	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 206  df-an 397  df-or 845  df-ex 1787  df-nf 1791

This theorem is referenced by:  nf3and  1905  nfan  1906  nfbid  1909  nfeud2  2592  nfeudw  2593  nfeld  2920  nfreud  3301  nfrmod  3302  nfreuwOLD  3305  nfrmowOLD  3306  nfrmo  3308  nfrabwOLD  3318  nfrab  3319  nfifd  4494  nfdisjw  5056  nfdisj  5057  nfopabd  5147  dfid3  5493  nfriotadw  7236  nfriotad  7240  axrepndlem1  10349  axrepndlem2  10350  axunndlem1  10352  axunnd  10353  axregndlem2  10360  axinfndlem1  10362  axinfnd  10363  axacndlem4  10367  axacndlem5  10368  axacnd  10369  bj-gabima  35124  cbvreud  35540  riotasv2d  36967