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

Theorem nfri 1455
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 1454 . 2  |-  ( F/ x ph  ->  ( ph  ->  A. x ph )
)
31, 2ax-mp 7 1  |-  ( ph  ->  A. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1285   F/wnf 1392
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-4 1443
This theorem depends on definitions:  df-bi 115  df-nf 1393
This theorem is referenced by:  alimd  1457  alrimi  1458  nfd  1459  nfrimi  1461  nfbidf  1475  19.3  1489  nfan1  1499  nfim1  1506  nfor  1509  nfal  1511  nfimd  1520  exlimi  1528  exlimd  1531  eximd  1546  albid  1549  exbid  1550  nfex  1571  19.9  1578  nf2  1601  nf3  1602  spim  1670  cbv2  1679  cbval  1681  cbvex  1683  nfald  1687  nfexd  1688  sbf  1704  nfs1f  1707  sbied  1715  sbie  1718  nfs1  1734  equs5or  1755  sb4or  1758  sbid2  1775  cbvexd  1847  hbsb  1868  sbco2yz  1882  sbco2  1884  sbco3v  1888  sbcomxyyz  1891  nfsbd  1896  hbeu  1966  mo23  1986  mor  1987  eu2  1989  eu3  1991  mo2r  1997  mo3  1999  mo2dc  2000  moexexdc  2029  nfsab  2077  nfcrii  2218  bj-sbime  11119
  Copyright terms: Public domain W3C validator