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

Theorem nfan1 2106
Description: A closed form of nfan 1868. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1750 changed. (Revised by Wolf Lammen, 18-Sep-2021.)
Hypotheses
Ref Expression
nfim1.1 𝑥𝜑
nfim1.2 (𝜑 → Ⅎ𝑥𝜓)
Assertion
Ref Expression
nfan1 𝑥(𝜑𝜓)

Proof of Theorem nfan1
StepHypRef Expression
1 df-an 385 . 2 ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
2 nfim1.1 . . . 4 𝑥𝜑
3 nfim1.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜓)
4 nfnt 1822 . . . . 5 (Ⅎ𝑥𝜓 → Ⅎ𝑥 ¬ 𝜓)
53, 4syl 17 . . . 4 (𝜑 → Ⅎ𝑥 ¬ 𝜓)
62, 5nfim1 2105 . . 3 𝑥(𝜑 → ¬ 𝜓)
76nfn 1824 . 2 𝑥 ¬ (𝜑 → ¬ 𝜓)
81, 7nfxfr 1819 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 383  wnf 1748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1745  df-nf 1750
This theorem is referenced by:  ralcom2  3133  sbcralt  3543  sbcrext  3544  sbcrextOLD  3545  csbiebt  3586  riota5f  6676  axrepndlem1  9452  axrepndlem2  9453  axunnd  9456  axpowndlem2  9458  axpowndlem3  9459  axpowndlem4  9460  axregndlem2  9463  axinfndlem1  9465  axinfnd  9466  axacndlem4  9470  axacndlem5  9471  axacnd  9472  fproddivf  14762  wl-sbcom2d-lem1  33472  wl-mo2df  33482  wl-eudf  33484  wl-mo3t  33488  wl-ax11-lem4  33495  wl-ax11-lem6  33497
  Copyright terms: Public domain W3C validator