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

Theorem nfan1 2030
 Description: A closed form of nfan 2031. (Contributed by Mario Carneiro, 3-Oct-2016.)
Hypotheses
Ref Expression
nfan1.1
nfan1.2
Assertion
Ref Expression
nfan1

Proof of Theorem nfan1
StepHypRef Expression
1 nfan1.2 . . . . 5
21nfrd 1973 . . . 4
32imdistani 704 . . 3
4 nfan1.1 . . . 4
5419.28 2027 . . 3
63, 5sylibr 217 . 2
76nfi 1682 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 376  wal 1450  wnf 1675 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-12 1950 This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-nf 1676 This theorem is referenced by:  nfan  2031  ralcom2  2941  sbcralt  3328  sbcrext  3329  csbiebt  3369  riota5f  6294  axrepndlem1  9035  axrepndlem2  9036  axunnd  9039  axpowndlem2  9041  axpowndlem3  9042  axpowndlem4  9043  axregndlem2  9046  axinfndlem1  9048  axinfnd  9049  axacndlem4  9053  axacndlem5  9054  axacnd  9055  fproddivf  14118  wl-sbcom2d-lem1  31959  wl-mo2df  31969  wl-eudf  31971  wl-mo3t  31975  wl-ax11-lem4  31982  wl-ax11-lem6  31984
 Copyright terms: Public domain W3C validator