ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfri Unicode version

Theorem nfri 1499
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 1498 . 2  |-  ( F/ x ph  ->  ( ph  ->  A. x ph )
)
31, 2ax-mp 5 1  |-  ( ph  ->  A. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1329   F/wnf 1436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-4 1487
This theorem depends on definitions:  df-bi 116  df-nf 1437
This theorem is referenced by:  alimd  1501  alrimi  1502  nfd  1503  nfrimi  1505  nfbidf  1519  19.3  1533  nfan1  1543  nfim1  1550  nfor  1553  nfal  1555  nfimd  1564  exlimi  1573  exlimd  1576  eximd  1591  albid  1594  exbid  1595  nfex  1616  19.9  1623  nf2  1646  nf3  1647  spim  1716  cbv2  1725  cbval  1727  cbvex  1729  nfald  1733  nfexd  1734  sbf  1750  nfs1f  1753  sbied  1761  sbie  1764  nfs1  1781  equs5or  1802  sb4or  1805  sbid2  1822  cbvexd  1899  hbsb  1922  sbco2yz  1936  sbco2  1938  sbco3v  1942  sbcomxyyz  1945  nfsbd  1950  hbeu  2020  mo23  2040  mor  2041  eu2  2043  eu3  2045  mo2r  2051  mo3  2053  mo2dc  2054  moexexdc  2083  nfsab  2131  nfcrii  2274  bj-sbime  13039
  Copyright terms: Public domain W3C validator