Theorem nfa1 1431

Description: x is not free in A.xph. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
nfa1	|- F/xA.xph

Proof of Theorem nfa1

Step	Hyp	Ref	Expression
1		hba1 1430	. 2 |- (A.xph -> A.xA.xph)
2	1	nfi 1348	1 |- F/xA.xph

Syntax hints:  A.wal 1240   F/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  9244  bdsepnft  9342  setindft  9425  strcollnft  9444