Theorem nfa1 1788

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 1786	. 2 |- (A.xph -> A.xA.xph)
2	1	nfi 1551	1 |- F/xA.xph

Syntax hints:  A.wal 1540   F/wnf 1544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-ex 1542  df-nf 1545

This theorem is referenced by:  a5i  1789  nfnf1  1790  nfimdOLD  1809  19.12  1847  nfa2  1855  nfia1  1856  19.21tOLD  1863  nf2  1866  19.38OLD  1874  equs5a  1887  nfald2  1972  spimt  1974  ax11v2  1992  equs5  1996  ax15  2021  sbf2  2028  nfsb4t  2080  sb56  2098  sbal1  2126  exsb  2130  nfeu1  2214  eupickbi  2270  moexex  2273  2eu1  2284  2eu4  2287  exists2  2294  axi12  2333  nfaba1  2494  nfra1  2664  ceqsalg  2883  csbie2t  3180  sbcnestgf  3183  dfnfc2  3909  ncfinlower  4483  copsex2t  4608  mosubopt  4612  ssopab2  4712  fv3  5341  fnoprabg  5585  mpteq12f  5655