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

Theorem nfri 1882
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 1881 . 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 1397   F/wnf 1624
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-12 1862
This theorem depends on definitions:  df-bi 185  df-ex 1621  df-nf 1625
This theorem is referenced by:  alimd  1884  alrimi  1885  eximd  1890  nexd  1891  albid  1893  exbid  1894  19.3  1896  19.9  1901  nfim1  1927  hban  1939  hb3an  1940  nfal  1955  nfex  1956  cbv2  2027  equs45f  2095  nfs1  2108  sb6f  2130  hbsb  2189  nfsab  2373  nfcrii  2536  hbra1  2764  ralrimi  2782  mpt2bi123f  30737  bnj1316  34226  bnj1379  34236  bnj1468  34251  bnj958  34345  bnj981  34355  bnj1014  34365  bnj1128  34393  bnj1204  34415  bnj1279  34421  bnj1398  34437  bnj1408  34439  bnj1444  34446  bnj1445  34447  bnj1446  34448  bnj1447  34449  bnj1448  34450  bnj1449  34451  bnj1463  34458  bnj1312  34461  bnj1518  34467  bnj1519  34468  bnj1520  34469  bnj1525  34472  bj-cbv2v  34642  bj-equs45fv  34678  bj-nfcrii  34774
  Copyright terms: Public domain W3C validator