MPE Home 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  |-  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 1779 . . . 4  |-  ( ph  ->  ( ps  ->  A. x ps ) )
32imdistani 672 . . 3  |-  ( (
ph  /\  ps )  ->  ( ph  /\  A. x ps ) )
4 nfan1.1 . . . 4  |-  F/ x ph
5419.28 1842 . . 3  |-  ( A. x ( ph  /\  ps )  <->  ( ph  /\  A. x ps ) )
63, 5sylibr 204 . 2  |-  ( (
ph  /\  ps )  ->  A. x ( ph  /\ 
ps ) )
76nfi 1560 1  |-  F/ x
( ph  /\  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   A.wal 1549   F/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