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

Theorem nfan1 1834
Description: A closed form of nfan 1783. (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 1755 . . . 4  |-  ( ph  ->  ( ps  ->  A. x ps ) )
32imdistani 671 . . 3  |-  ( (
ph  /\  ps )  ->  ( ph  /\  A. x ps ) )
4 nfim1.1 . . . 4  |-  F/ x ph
5419.28 1818 . . 3  |-  ( A. x ( ph  /\  ps )  <->  ( ph  /\  A. x ps ) )
63, 5sylibr 203 . 2  |-  ( (
ph  /\  ps )  ->  A. x ( ph  /\ 
ps ) )
76nfi 1541 1  |-  F/ x
( ph  /\  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358   A.wal 1530   F/wnf 1534
This theorem is referenced by:  spimed  1930  ralcom2  2717  sbcralt  3076  sbcrext  3077  csbiebt  3130  riota5f  6345  riotasvdOLD  6364  axrepndlem1  8230  axrepndlem2  8231  axunnd  8234  axpowndlem2  8236  axpowndlem4  8238  axregndlem2  8241  axinfndlem1  8243  axinfnd  8244  axacndlem4  8248  axacndlem5  8249  axacnd  8250  spimedNEW7  29487
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-nf 1535
  Copyright terms: Public domain W3C validator