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

Theorem nfan1 1822
Description: A closed form of nfan 1771. (Contributed by Mario Carneiro, 3-Oct-2016.)
Hypotheses
Ref Expression
nfim1.1  |-  F/ x ph
nfim1.2  |-  ( ph  ->  F/ x ps )
Assertion
Ref Expression
nfan1  |-  F/ x
( ph  /\  ps )

Proof of Theorem nfan1
StepHypRef Expression
1 nfim1.2 . . . . 5  |-  ( ph  ->  F/ x ps )
21nfrd 1743 . . . 4  |-  ( ph  ->  ( ps  ->  A. x ps ) )
32imdistani 671 . . 3  |-  ( (
ph  /\  ps )  ->  ( ph  /\  A. x ps ) )
4 nfim1.1 . . . 4  |-  F/ x ph
5419.28 1806 . . 3  |-  ( A. x ( ph  /\  ps )  <->  ( ph  /\  A. x ps ) )
63, 5sylibr 203 . 2  |-  ( (
ph  /\  ps )  ->  A. x ( ph  /\ 
ps ) )
76nfi 1538 1  |-  F/ x
( ph  /\  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   A.wal 1527   F/wnf 1531
This theorem is referenced by:  spimed  1917  ralcom2  2704  sbcralt  3063  sbcrext  3064  csbiebt  3117  riota5f  6329  riotasvdOLD  6348  axrepndlem1  8214  axrepndlem2  8215  axunnd  8218  axpowndlem2  8220  axpowndlem4  8222  axregndlem2  8225  axinfndlem1  8227  axinfnd  8228  axacndlem4  8232  axacndlem5  8233  axacnd  8234
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1532
  Copyright terms: Public domain W3C validator