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  2495  nfra1  2665  ceqsalg  2884  csbie2t  3181  sbcnestgf  3184  dfnfc2  3910  ncfinlower  4484  copsex2t  4609  mosubopt  4613  ssopab2  4713  fv3  5342  fnoprabg  5586  mpteq12f  5656