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

Theorem nfri 1874
 Description: Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfri.1
Assertion
Ref Expression
nfri

Proof of Theorem nfri
StepHypRef Expression
1 nfri.1 . 2
2 nfr 1873 . 2
31, 2ax-mp 5 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  A.wal 1393  F/wnf 1616 This theorem is referenced by:  alimd  1876  alrimi  1877  eximd  1882  nexd  1883  albid  1885  exbid  1886  19.3  1888  19.9  1893  nfim1  1919  hban  1931  hb3an  1932  nfal  1947  nfex  1948  cbv2  2020  equs45f  2091  nfs1  2104  sb6f  2126  hbsb  2185  nfsab  2448  nfcrii  2611  hbra1  2839  ralrimi  2857  mpt2bi123f  30571  bnj1316  33879  bnj1379  33889  bnj1468  33904  bnj958  33998  bnj981  34008  bnj1014  34018  bnj1128  34046  bnj1204  34068  bnj1279  34074  bnj1398  34090  bnj1408  34092  bnj1444  34099  bnj1445  34100  bnj1446  34101  bnj1447  34102  bnj1448  34103  bnj1449  34104  bnj1463  34111  bnj1312  34114  bnj1518  34120  bnj1519  34121  bnj1520  34122  bnj1525  34125  bj-cbv2v  34295  bj-equs45fv  34331  bj-nfcrii  34427 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854 This theorem depends on definitions:  df-bi 185  df-ex 1613  df-nf 1617
 Copyright terms: Public domain W3C validator