Theorem nf5ri 2065

Description: Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis

Ref	Expression
nf5ri.1	|- F/ x ph

Assertion

Ref	Expression
nf5ri	|- ( ph -> A. x ph )

Proof of Theorem nf5ri

Step	Hyp	Ref	Expression
1		nf5ri.1	. 2 |- F/ x ph
2		nf5r 2064	. 2 |- ( F/ x ph -> ( ph -> A. x ph ) )
3	1, 2	ax-mp 5	1 |- ( ph -> A. x ph )

Syntax hints:   -> wi 4   A.wal 1481   F/wnf 1708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-ex 1705  df-nf 1710

This theorem is referenced by:  19.3  2069  alimd  2081  alrimi  2082  eximd  2085  nexd  2089  albid  2090  exbid  2091  hban  2128  hb3an  2129  hba1  2151  nfal  2153  nfexOLD  2155  hbex  2156  cbv2  2270  equs45f  2350  nfs1  2365  sb6f  2385  hbsb  2441  nfsab  2614  nfcrii  2757  hbra1  2942  ralrimi  2957  bnj1316  30891  bnj1379  30901  bnj1468  30916  bnj958  31010  bnj981  31020  bnj1014  31030  bnj1128  31058  bnj1204  31080  bnj1279  31086  bnj1398  31102  bnj1408  31104  bnj1444  31111  bnj1445  31112  bnj1446  31113  bnj1447  31114  bnj1448  31115  bnj1449  31116  bnj1463  31123  bnj1312  31126  bnj1518  31132  bnj1519  31133  bnj1520  31134  bnj1525  31137  bj-cbv2v  32732  bj-equs45fv  32752  bj-nfcrii  32851  mpt2bi123f  33971