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

Theorem nfan1 1982
Description: A closed form of nfan 1983. (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 1925 . . . 4  |-  ( ph  ->  ( ps  ->  A. x ps ) )
32imdistani 694 . . 3  |-  ( (
ph  /\  ps )  ->  ( ph  /\  A. x ps ) )
4 nfan1.1 . . . 4  |-  F/ x ph
5419.28 1979 . . 3  |-  ( A. x ( ph  /\  ps )  <->  ( ph  /\  A. x ps ) )
63, 5sylibr 215 . 2  |-  ( (
ph  /\  ps )  ->  A. x ( ph  /\ 
ps ) )
76nfi 1670 1  |-  F/ x
( ph  /\  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370   A.wal 1435   F/wnf 1663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-12 1904
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-nf 1664
This theorem is referenced by:  nfan  1983  ralcom2  2991  sbcralt  3369  sbcrext  3370  csbiebt  3412  riota5f  6282  axrepndlem1  9006  axrepndlem2  9007  axunnd  9010  axpowndlem2  9012  axpowndlem3  9013  axpowndlem4  9014  axregndlem2  9017  axinfndlem1  9019  axinfnd  9020  axacndlem4  9024  axacndlem5  9025  axacnd  9026  fproddivf  14008  wl-sbcom2d-lem1  31637  wl-mo2df  31647  wl-eudf  31649  wl-mo3t  31653  wl-ax11-lem4  31666  wl-ax11-lem6  31668
  Copyright terms: Public domain W3C validator