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

Theorem nfand 1892
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 399 . 2 ((𝜓𝜒) ↔ ¬ (𝜓 → ¬ 𝜒))
2 nfand.1 . . . 4 (𝜑 → Ⅎ𝑥𝜓)
3 nfand.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜒)
43nfnd 1852 . . . 4 (𝜑 → Ⅎ𝑥 ¬ 𝜒)
52, 4nfimd 1889 . . 3 (𝜑 → Ⅎ𝑥(𝜓 → ¬ 𝜒))
65nfnd 1852 . 2 (𝜑 → Ⅎ𝑥 ¬ (𝜓 → ¬ 𝜒))
71, 6nfxfrd 1848 1 (𝜑 → Ⅎ𝑥(𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 398  wnf 1778
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1775  df-nf 1779
This theorem is referenced by:  nf3and  1893  nfan  1894  nfbid  1897  nfeud2  2670  nfeudw  2671  nfeld  2987  nfreud  3371  nfrmod  3372  nfreuw  3373  nfrmow  3374  nfrmo  3376  nfrabw  3384  nfrab  3385  nfifd  4493  nfdisjw  5034  nfdisj  5035  dfid3  5455  nfriotadw  7114  nfriotad  7117  axrepndlem1  10006  axrepndlem2  10007  axunndlem1  10009  axunnd  10010  axregndlem2  10017  axinfndlem1  10019  axinfnd  10020  axacndlem4  10024  axacndlem5  10025  axacnd  10026  cbvreud  34646  riotasv2d  36085
  Copyright terms: Public domain W3C validator