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

Theorem nfan1 1845
 Description: A closed form of nfan 1846. (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 1779 . . . 4
32imdistani 672 . . 3
4 nfan1.1 . . . 4
5419.28 1842 . . 3
63, 5sylibr 204 . 2
76nfi 1560 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 359  wal 1549  wnf 1553 This theorem is referenced by:  nfan  1846  spimedOLD  1961  ralcom2  2864  sbcralt  3225  sbcrext  3226  csbiebt  3279  riota5f  6566  riotasvdOLD  6585  axrepndlem1  8457  axrepndlem2  8458  axunnd  8461  axpowndlem2  8463  axpowndlem4  8465  axregndlem2  8468  axinfndlem1  8470  axinfnd  8471  axacndlem4  8475  axacndlem5  8476  axacnd  8477  spimedNEW7  29411 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761 This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554
 Copyright terms: Public domain W3C validator