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

Theorem nfand 1901
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 398 . 2 ((𝜓𝜒) ↔ ¬ (𝜓 → ¬ 𝜒))
2 nfand.1 . . . 4 (𝜑 → Ⅎ𝑥𝜓)
3 nfand.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜒)
43nfnd 1862 . . . 4 (𝜑 → Ⅎ𝑥 ¬ 𝜒)
52, 4nfimd 1898 . . 3 (𝜑 → Ⅎ𝑥(𝜓 → ¬ 𝜒))
65nfnd 1862 . 2 (𝜑 → Ⅎ𝑥 ¬ (𝜓 → ¬ 𝜒))
71, 6nfxfrd 1857 1 (𝜑 → Ⅎ𝑥(𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 397  wnf 1786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-nf 1787
This theorem is referenced by:  nf3and  1902  nfan  1903  nfbid  1906  nfeud2  2585  nfeudw  2586  nfeld  2915  nfreuwOLD  3423  nfrmowOLD  3424  nfrmod  3429  nfreud  3430  nfrmo  3431  nfrabwOLD  3470  nfrab  3473  nfifd  4558  nfdisjw  5126  nfdisj  5127  nfopabd  5217  dfid3  5578  nfriotadw  7373  nfriotad  7377  axrepndlem1  10587  axrepndlem2  10588  axunndlem1  10590  axunnd  10591  axregndlem2  10598  axinfndlem1  10600  axinfnd  10601  axacndlem4  10605  axacndlem5  10606  axacnd  10607  bj-gabima  35820  cbvreud  36254  riotasv2d  37827
  Copyright terms: Public domain W3C validator