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

Theorem nfa1 1431
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 1430 . 2 (xφxxφ)
21nfi 1348 1 xxφ
Colors of variables: wff set class
Syntax hints:  wal 1240  wnf 1346
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 1335  ax-ial 1424
This theorem depends on definitions:  df-bi 110  df-nf 1347
This theorem is referenced by:  nfnf1  1433  nfa2  1468  nfia1  1469  alexdc  1507  nf2  1555  cbv1h  1630  sbf2  1658  sb4or  1711  nfsbxy  1815  nfsbxyt  1816  sbcomxyyz  1843  sbalyz  1872  dvelimALT  1883  nfeu1  1908  moim  1961  euexex  1982  nfaba1  2180  nfra1  2349  ceqsalg  2576  elrab3t  2691  mo2icl  2714  csbie2t  2888  sbcnestgf  2891  dfnfc2  3589  mpteq12f  3828  copsex2t  3973  ssopab2  4003  alxfr  4159  eunex  4239  mosubopt  4348  fv3  5140  fvmptt  5205  fnoprabg  5544  bj-exlimmp  9178  bdsepnft  9275  setindft  9349  strcollnft  9368
  Copyright terms: Public domain W3C validator