MPE Home 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  |-  F/ x ph
nfan1.2  |-  ( ph  ->  F/ x ps )
Assertion
Ref Expression
nfan1  |-  F/ x
( ph  /\  ps )

Proof of Theorem nfan1
StepHypRef Expression
1 nfan1.2 . . . . 5  |-  ( ph  ->  F/ x ps )
21nfrd 1973 . . . 4  |-  ( ph  ->  ( ps  ->  A. x ps ) )
32imdistani 704 . . 3  |-  ( (
ph  /\  ps )  ->  ( ph  /\  A. x ps ) )
4 nfan1.1 . . . 4  |-  F/ x ph
5419.28 2027 . . 3  |-  ( A. x ( ph  /\  ps )  <->  ( ph  /\  A. x ps ) )
63, 5sylibr 217 . 2  |-  ( (
ph  /\  ps )  ->  A. x ( ph  /\ 
ps ) )
76nfi 1682 1  |-  F/ x
( ph  /\  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376   A.wal 1450   F/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