MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfand Structured version   Visualization version   GIF version

Theorem nfand 1997
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
StepHypRef Expression
1 df-an 386 . 2 ((𝜓𝜒) ↔ ¬ (𝜓 → ¬ 𝜒))
2 nfand.1 . . . 4 (𝜑 → Ⅎ𝑥𝜓)
3 nfand.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜒)
43nfnd 1955 . . . 4 (𝜑 → Ⅎ𝑥 ¬ 𝜒)
52, 4nfimd 1993 . . 3 (𝜑 → Ⅎ𝑥(𝜓 → ¬ 𝜒))
65nfnd 1955 . 2 (𝜑 → Ⅎ𝑥 ¬ (𝜓 → ¬ 𝜒))
71, 6nfxfrd 1950 1 (𝜑 → Ⅎ𝑥(𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 385  wnf 1879
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-ex 1876  df-nf 1880
This theorem is referenced by:  nf3and  1998  nfan  1999  nfbid  2002  nfeud2  2630  nfeld  2950  nfreud  3293  nfrmod  3294  nfrmo  3296  nfrab  3305  nfifd  4305  nfdisj  4823  dfid3  5221  nfriotad  6847  axrepndlem1  9702  axrepndlem2  9703  axunndlem1  9705  axunnd  9706  axregndlem2  9713  axinfndlem1  9715  axinfnd  9716  axacndlem4  9720  axacndlem5  9721  axacnd  9722  riotasv2d  34978
  Copyright terms: Public domain W3C validator