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

Theorem nfan1 2066
Description: A closed form of nfan 1825. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1707 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 386 . 2 ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
2 nfim1.1 . . . 4 𝑥𝜑
3 nfim1.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜓)
4 nfnt 1779 . . . . 5 (Ⅎ𝑥𝜓 → Ⅎ𝑥 ¬ 𝜓)
53, 4syl 17 . . . 4 (𝜑 → Ⅎ𝑥 ¬ 𝜓)
62, 5nfim1 2065 . . 3 𝑥(𝜑 → ¬ 𝜓)
76nfn 1781 . 2 𝑥 ¬ (𝜑 → ¬ 𝜓)
81, 7nfxfr 1776 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  wnf 1705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-12 2044
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1702  df-nf 1707
This theorem is referenced by:  ralcom2  3094  sbcralt  3492  sbcrext  3493  sbcrextOLD  3494  csbiebt  3534  riota5f  6590  axrepndlem1  9358  axrepndlem2  9359  axunnd  9362  axpowndlem2  9364  axpowndlem3  9365  axpowndlem4  9366  axregndlem2  9369  axinfndlem1  9371  axinfnd  9372  axacndlem4  9376  axacndlem5  9377  axacnd  9378  fproddivf  14643  wl-sbcom2d-lem1  32971  wl-mo2df  32981  wl-eudf  32983  wl-mo3t  32987  wl-ax11-lem4  32994  wl-ax11-lem6  32996
  Copyright terms: Public domain W3C validator