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

Theorem nfand 1895
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 1856 . . . 4 (𝜑 → Ⅎ𝑥 ¬ 𝜒)
52, 4nfimd 1892 . . 3 (𝜑 → Ⅎ𝑥(𝜓 → ¬ 𝜒))
65nfnd 1856 . 2 (𝜑 → Ⅎ𝑥 ¬ (𝜓 → ¬ 𝜒))
71, 6nfxfrd 1851 1 (𝜑 → Ⅎ𝑥(𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wnf 1780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1777  df-nf 1781
This theorem is referenced by:  nf3and  1896  nfan  1897  nfbid  1900  nfeud2  2588  nfeudw  2589  nfeld  2915  nfreuwOLD  3423  nfrmowOLD  3424  nfrmod  3429  nfreud  3430  nfrmo  3431  nfrabwOLD  3474  nfrab  3476  nfifd  4560  nfdisjw  5127  nfdisj  5128  nfopabd  5216  dfid3  5586  nfriotadw  7396  nfriotad  7399  axrepndlem1  10630  axrepndlem2  10631  axunndlem1  10633  axunnd  10634  axregndlem2  10641  axinfndlem1  10643  axinfnd  10644  axacndlem4  10648  axacndlem5  10649  axacnd  10650  axsepg2  35075  axsepg2ALT  35076  bj-gabima  36923  cbvreud  37356  riotasv2d  38939
  Copyright terms: Public domain W3C validator