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

Theorem nfri 1810
Description: Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfri.1  |-  F/ x ph
Assertion
Ref Expression
nfri  |-  ( ph  ->  A. x ph )

Proof of Theorem nfri
StepHypRef Expression
1 nfri.1 . 2  |-  F/ x ph
2 nfr 1809 . 2  |-  ( F/ x ph  ->  ( ph  ->  A. x ph )
)
31, 2ax-mp 5 1  |-  ( ph  ->  A. x ph )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   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-ex 1588  df-nf 1591
This theorem is referenced by:  alimd  1812  alrimi  1813  eximd  1818  nexd  1819  albid  1821  exbid  1822  19.3  1824  19.9  1829  nfim1  1854  hban  1866  hb3an  1867  nfal  1882  nfex  1883  cbv2  1976  equs45f  2048  nfs1  2061  sb6f  2083  hbsb  2154  nfsab  2442  nfcrii  2605  cleqf  2639  ralrimi  2815  ralimdaa  2818  ralbida  2833  exlimddvf  29069  mpt2bi123f  29115  bnj1316  32116  bnj1379  32126  bnj1468  32141  bnj958  32235  bnj981  32245  bnj1014  32255  bnj1128  32283  bnj1204  32305  bnj1279  32311  bnj1398  32327  bnj1408  32329  bnj1444  32336  bnj1445  32337  bnj1446  32338  bnj1447  32339  bnj1448  32340  bnj1449  32341  bnj1463  32348  bnj1312  32351  bnj1518  32357  bnj1519  32358  bnj1520  32359  bnj1525  32362  bj-cbv2v  32533  bj-equs45fv  32568  bj-nfcrii  32664
  Copyright terms: Public domain W3C validator