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

Theorem nfri 1428
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 1427 . 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 1257   F/wnf 1365
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-4 1416
This theorem depends on definitions:  df-bi 114  df-nf 1366
This theorem is referenced by:  alimd  1430  alrimi  1431  nfd  1432  nfrimi  1434  nfbidf  1448  19.3  1462  nfan1  1472  nfim1  1479  nfor  1482  nfal  1484  nfimd  1493  exlimi  1501  exlimd  1504  eximd  1519  albid  1522  exbid  1523  nfex  1544  19.9  1551  nf2  1574  nf3  1575  spim  1642  cbv2  1651  cbval  1653  cbvex  1655  nfald  1659  nfexd  1660  sbf  1676  nfs1f  1679  sbied  1687  sbie  1690  nfs1  1706  equs5or  1727  sb4or  1730  sbid2  1746  cbvexd  1818  hbsb  1839  sbco2yz  1853  sbco2  1855  sbco3v  1859  sbcomxyyz  1862  nfsbd  1867  hbeu  1937  mo23  1957  mor  1958  eu2  1960  eu3  1962  mo2r  1968  mo3  1970  mo2dc  1971  moexexdc  2000  nfsab  2048  nfcrii  2187  bj-sbime  10300
  Copyright terms: Public domain W3C validator