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

Theorem nfan1 1835
Description: A closed form of nfan 1836. (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 1771 . . . 4  |-  ( ph  ->  ( ps  ->  A. x ps ) )
32imdistani 672 . . 3  |-  ( (
ph  /\  ps )  ->  ( ph  /\  A. x ps ) )
4 nfan1.1 . . . 4  |-  F/ x ph
5419.28 1832 . . 3  |-  ( A. x ( ph  /\  ps )  <->  ( ph  /\  A. x ps ) )
63, 5sylibr 204 . 2  |-  ( (
ph  /\  ps )  ->  A. x ( ph  /\ 
ps ) )
76nfi 1557 1  |-  F/ x
( ph  /\  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   A.wal 1546   F/wnf 1550
This theorem is referenced by:  nfan  1836  spimed  2003  ralcom2  2808  sbcralt  3169  sbcrext  3170  csbiebt  3223  riota5f  6503  riotasvdOLD  6522  axrepndlem1  8393  axrepndlem2  8394  axunnd  8397  axpowndlem2  8399  axpowndlem4  8401  axregndlem2  8404  axinfndlem1  8406  axinfnd  8407  axacndlem4  8411  axacndlem5  8412  axacnd  8413  spimedNEW7  28841
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator