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

Theorem nfan1 2182
Description: A closed form of nfan 1946. (Contributed by Mario Carneiro, 3-Oct-2016.) df-nf 1828 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 387 . 2 ((𝜑𝜓) ↔ ¬ (𝜑 → ¬ 𝜓))
2 nfim1.1 . . . 4 𝑥𝜑
3 nfim1.2 . . . . 5 (𝜑 → Ⅎ𝑥𝜓)
43nfnd 1903 . . . 4 (𝜑 → Ⅎ𝑥 ¬ 𝜓)
52, 4nfim1 2181 . . 3 𝑥(𝜑 → ¬ 𝜓)
65nfn 1902 . 2 𝑥 ¬ (𝜑 → ¬ 𝜓)
71, 6nfxfr 1897 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 386  wnf 1827
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-12 2162
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-ex 1824  df-nf 1828
This theorem is referenced by:  ralcom2  3289  sbcralt  3727  sbcrext  3728  csbiebt  3770  riota5f  6908  axrepndlem1  9749  axrepndlem2  9750  axunnd  9753  axpowndlem2  9755  axpowndlem3  9756  axpowndlem4  9757  axregndlem2  9760  axinfndlem1  9762  axinfnd  9763  axacndlem4  9767  axacndlem5  9768  axacnd  9769  fproddivf  15120  wl-sbcom2d-lem1  33950  wl-mo2df  33960  wl-eudf  33962  wl-mo3t  33966  wl-ax11-lem4  33973  wl-ax11-lem6  33975
  Copyright terms: Public domain W3C validator