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

Theorem nfri 1962
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 1961 . 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 1452   F/wnf 1677
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-12 1943
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1674  df-nf 1678
This theorem is referenced by:  alimd  1964  alrimi  1965  eximd  1970  nexd  1971  albid  1973  exbid  1974  19.3  1976  19.9OLD  1985  nfim1  2012  hban  2024  hb3an  2025  nfal  2040  nfex  2041  cbv2  2123  equs45f  2191  nfs1  2204  sb6f  2224  hbsb  2280  nfsab  2453  nfcrii  2595  hbra1  2781  ralrimi  2799  bnj1316  29680  bnj1379  29690  bnj1468  29705  bnj958  29799  bnj981  29809  bnj1014  29819  bnj1128  29847  bnj1204  29869  bnj1279  29875  bnj1398  29891  bnj1408  29893  bnj1444  29900  bnj1445  29901  bnj1446  29902  bnj1447  29903  bnj1448  29904  bnj1449  29905  bnj1463  29912  bnj1312  29915  bnj1518  29921  bnj1519  29922  bnj1520  29923  bnj1525  29926  bj-cbv2v  31377  bj-equs45fv  31407  bj-nfcrii  31504  mpt2bi123f  32450
  Copyright terms: Public domain W3C validator