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

Theorem nfan1 1874
Description: A closed form of nfan 1875. (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 1823 . . . 4  |-  ( ph  ->  ( ps  ->  A. x ps ) )
32imdistani 690 . . 3  |-  ( (
ph  /\  ps )  ->  ( ph  /\  A. x ps ) )
4 nfan1.1 . . . 4  |-  F/ x ph
5419.28 1871 . . 3  |-  ( A. x ( ph  /\  ps )  <->  ( ph  /\  A. x ps ) )
63, 5sylibr 212 . 2  |-  ( (
ph  /\  ps )  ->  A. x ( ph  /\ 
ps ) )
76nfi 1606 1  |-  F/ x
( ph  /\  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   A.wal 1377   F/wnf 1599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600
This theorem is referenced by:  nfan  1875  ralcom2  3026  sbcralt  3412  sbcrextOLD  3413  sbcrext  3414  csbiebt  3455  riota5f  6271  axrepndlem1  8968  axrepndlem2  8969  axunnd  8972  axpowndlem2  8974  axpowndlem2OLD  8975  axpowndlem3  8976  axpowndlem4  8978  axregndlem2  8981  axinfndlem1  8984  axinfnd  8985  axacndlem4  8989  axacndlem5  8990  axacnd  8991  wl-sbcom2d-lem1  29862  wl-mo2dnae  29872  wl-mo3t  29874  wl-ax11-lem4  29881  wl-ax11-lem6  29883
  Copyright terms: Public domain W3C validator