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

Theorem nfand 1823
 Description: If in a context 𝑥 is not free in 𝜓 and 𝜒, 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 1782 . . . 4 (𝜑 → Ⅎ𝑥 ¬ 𝜒)
52, 4nfimd 1820 . . 3 (𝜑 → Ⅎ𝑥(𝜓 → ¬ 𝜒))
65nfnd 1782 . 2 (𝜑 → Ⅎ𝑥 ¬ (𝜓 → ¬ 𝜒))
71, 6nfxfrd 1777 1 (𝜑 → Ⅎ𝑥(𝜓𝜒))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 384  Ⅎwnf 1705 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1702  df-nf 1707 This theorem is referenced by:  nf3and  1824  nfan  1825  nfbid  1829  nfeld  2769  nfreud  3106  nfrmod  3107  nfrmo  3109  nfrab  3116  nfifd  4092  nfdisj  4605  dfid3  5000  nfriotad  6584  axrepndlem1  9374  axrepndlem2  9375  axunndlem1  9377  axunnd  9378  axregndlem2  9385  axinfndlem1  9387  axinfnd  9388  axacndlem4  9392  axacndlem5  9393  axacnd  9394  riotasv2d  33762
 Copyright terms: Public domain W3C validator