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

Theorem nfri 1929
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 1928 . 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 1435   F/wnf 1661
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-12 1909
This theorem depends on definitions:  df-bi 188  df-ex 1658  df-nf 1662
This theorem is referenced by:  alimd  1931  alrimi  1932  eximd  1937  nexd  1938  albid  1940  exbid  1941  19.3  1943  19.9OLD  1952  nfim1  1979  hban  1991  hb3an  1992  nfal  2007  nfex  2008  cbv2  2085  equs45f  2155  nfs1  2168  sb6f  2190  hbsb  2247  nfsab  2420  nfcrii  2562  hbra1  2747  ralrimi  2765  bnj1316  29584  bnj1379  29594  bnj1468  29609  bnj958  29703  bnj981  29713  bnj1014  29723  bnj1128  29751  bnj1204  29773  bnj1279  29779  bnj1398  29795  bnj1408  29797  bnj1444  29804  bnj1445  29805  bnj1446  29806  bnj1447  29807  bnj1448  29808  bnj1449  29809  bnj1463  29816  bnj1312  29819  bnj1518  29825  bnj1519  29826  bnj1520  29827  bnj1525  29830  bj-cbv2v  31238  bj-equs45fv  31271  bj-nfcrii  31371  mpt2bi123f  32313
  Copyright terms: Public domain W3C validator