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

Theorem nfand 1896
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 396 . 2 ((𝜓𝜒) ↔ ¬ (𝜓 → ¬ 𝜒))
2 nfand.1 . . . 4 (𝜑 → Ⅎ𝑥𝜓)
3 nfand.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜒)
43nfnd 1857 . . . 4 (𝜑 → Ⅎ𝑥 ¬ 𝜒)
52, 4nfimd 1893 . . 3 (𝜑 → Ⅎ𝑥(𝜓 → ¬ 𝜒))
65nfnd 1857 . 2 (𝜑 → Ⅎ𝑥 ¬ (𝜓 → ¬ 𝜒))
71, 6nfxfrd 1853 1 (𝜑 → Ⅎ𝑥(𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wnf 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1779  df-nf 1783
This theorem is referenced by:  nf3and  1897  nfan  1898  nfbid  1901  nfeud2  2589  nfeudw  2590  nfeld  2916  nfreuwOLD  3425  nfrmowOLD  3426  nfrmod  3431  nfreud  3432  nfrmo  3433  nfrabwOLD  3475  nfrab  3477  nfifd  4554  nfdisjw  5121  nfdisj  5122  nfopabd  5210  dfid3  5580  nfriotadw  7397  nfriotad  7400  axrepndlem1  10633  axrepndlem2  10634  axunndlem1  10636  axunnd  10637  axregndlem2  10644  axinfndlem1  10646  axinfnd  10647  axacndlem4  10651  axacndlem5  10652  axacnd  10653  axsepg2  35097  axsepg2ALT  35098  bj-gabima  36942  cbvreud  37375  riotasv2d  38959
  Copyright terms: Public domain W3C validator