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

Theorem nfan1 2056
 Description: A closed form of nfan 1816. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1701 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 1767 . . . . 5 (Ⅎ𝑥𝜓 → Ⅎ𝑥 ¬ 𝜓)
53, 4syl 17 . . . 4 (𝜑 → Ⅎ𝑥 ¬ 𝜓)
62, 5nfim1 2055 . . 3 𝑥(𝜑 → ¬ 𝜓)
76nfn 1768 . 2 𝑥 ¬ (𝜑 → ¬ 𝜓)
81, 7nfxfr 1771 1 𝑥(𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383  Ⅎwnf 1699 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-ex 1696  df-nf 1701 This theorem is referenced by:  ralcom2  3083  sbcralt  3477  sbcrext  3478  sbcrextOLD  3479  csbiebt  3519  riota5f  6535  axrepndlem1  9293  axrepndlem2  9294  axunnd  9297  axpowndlem2  9299  axpowndlem3  9300  axpowndlem4  9301  axregndlem2  9304  axinfndlem1  9306  axinfnd  9307  axacndlem4  9311  axacndlem5  9312  axacnd  9313  fproddivf  14557  wl-sbcom2d-lem1  32521  wl-mo2df  32531  wl-eudf  32533  wl-mo3t  32537  wl-ax11-lem4  32544  wl-ax11-lem6  32546
 Copyright terms: Public domain W3C validator