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

Theorem nfan1 2188
Description: A closed form of nfan 1894. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1778 changed. (Revised by Wolf Lammen, 18-Sep-2021.) (Proof shortened by Wolf Lammen, 7-Jul-2022.)
Hypotheses
Ref Expression
nfim1.1 𝑥𝜑
nfim1.2 (𝜑 → Ⅎ𝑥𝜓)
Assertion
Ref Expression
nfan1 𝑥(𝜑𝜓)

Proof of Theorem nfan1
StepHypRef Expression
1 df-an 395 . 2 ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
2 nfim1.1 . . . 4 𝑥𝜑
3 nfim1.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜓)
43nfnd 1853 . . . 4 (𝜑 → Ⅎ𝑥 ¬ 𝜓)
52, 4nfim1 2187 . . 3 𝑥(𝜑 → ¬ 𝜓)
65nfn 1852 . 2 𝑥 ¬ (𝜑 → ¬ 𝜓)
71, 6nfxfr 1847 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394  wnf 1777
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-12 2166
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1774  df-nf 1778
This theorem is referenced by:  sb4b  2468  ralcom2  3360  sbcralt  3862  sbcrext  3863  csbiebt  3919  riota5f  7404  axrepndlem1  10617  axrepndlem2  10618  axunnd  10621  axpowndlem2  10623  axpowndlem3  10624  axpowndlem4  10625  axregndlem2  10628  axinfndlem1  10630  axinfnd  10631  axacndlem4  10635  axacndlem5  10636  axacnd  10637  fproddivf  15967  wl-sbcom2d-lem1  37157  wl-mo2df  37168  wl-eudf  37170  wl-mo3t  37174  wl-ax11-lem4  37186  wl-ax11-lem6  37188
  Copyright terms: Public domain W3C validator