ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfa1 Structured version   GIF version

Theorem nfa1 1416
Description: x is not free in xφ. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfa1 xxφ

Proof of Theorem nfa1
StepHypRef Expression
1 hba1 1415 . 2 (xφxxφ)
21nfi 1331 1 xxφ
Colors of variables: wff set class
Syntax hints:  wal 1226  wnf 1329
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1318  ax-ial 1409
This theorem depends on definitions:  df-bi 110  df-nf 1330
This theorem is referenced by:  nfnf1  1418  nfa2  1453  nfia1  1454  alexdc  1492  nf2  1540  cbv1h  1615  sbf2  1643  sb4or  1696  nfsbxy  1800  nfsbxyt  1801  sbcomxyyz  1828  sbalyz  1857  dvelimALT  1868  nfeu1  1893  moim  1946  euexex  1967  nfaba1  2165  nfra1  2333  ceqsalg  2559  elrab3t  2674  mo2icl  2697  csbie2t  2871  sbcnestgf  2874  dfnfc2  3572  mpteq12f  3811  copsex2t  3956  ssopab2  3986  alxfr  4143  eunex  4223  mosubopt  4332  fv3  5122  fvmptt  5187  fnoprabg  5525  bj-exlimmp  7016  bdsepnft  7113  setindft  7183  strcollnft  7202
  Copyright terms: Public domain W3C validator