Theorem nfe1 1382

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

Assertion

Ref	Expression
nfe1	|- F/xE.xph

Proof of Theorem nfe1

Step	Hyp	Ref	Expression
1		hbe1 1381	. 2 |- (E.xph -> A.xE.xph)
2	1	nfi 1348	1 |- F/xE.xph

Syntax hints:   F/wnf 1346  E.wex 1378

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-ie1 1379

This theorem depends on definitions:  df-bi 110  df-nf 1347

This theorem is referenced by:  nf3  1556  sb4or  1711  nfmo1  1909  euexex  1982  2moswapdc  1987  nfre1  2359  ceqsexg  2666  morex  2719  sbc6g  2782  rgenm  3317  intab  3635  nfopab1  3817  nfopab2  3818  copsexg  3972  copsex2t  3973  copsex2g  3974  eusv2nf  4154  mosubopt  4348  dmcoss  4544  imadif  4922  funimaexglem  4925  nfoprab1  5496  nfoprab2  5497  nfoprab3  5498