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

Theorem nfan1 1865
Description: A closed form of nfan 1866. (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 1814 . . . 4  |-  ( ph  ->  ( ps  ->  A. x ps ) )
32imdistani 690 . . 3  |-  ( (
ph  /\  ps )  ->  ( ph  /\  A. x ps ) )
4 nfan1.1 . . . 4  |-  F/ x ph
5419.28 1862 . . 3  |-  ( A. x ( ph  /\  ps )  <->  ( ph  /\  A. x ps ) )
63, 5sylibr 212 . 2  |-  ( (
ph  /\  ps )  ->  A. x ( ph  /\ 
ps ) )
76nfi 1597 1  |-  F/ x
( ph  /\  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   A.wal 1368   F/wnf 1590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591
This theorem is referenced by:  nfan  1866  ralcom2  2991  sbcralt  3375  sbcrextOLD  3376  sbcrext  3377  csbiebt  3418  riota5f  6189  axrepndlem1  8870  axrepndlem2  8871  axunnd  8874  axpowndlem2  8876  axpowndlem2OLD  8877  axpowndlem3  8878  axpowndlem4  8880  axregndlem2  8883  axinfndlem1  8886  axinfnd  8887  axacndlem4  8891  axacndlem5  8892  axacnd  8893  wl-sbcom2d-lem1  28553  wl-mo2dnae  28563  wl-mo3t  28565  wl-ax11-lem4  28572  wl-ax11-lem6  28574
  Copyright terms: Public domain W3C validator