Theorem hbe1 1381

Description: x is not free in E.xph. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
hbe1	|- (E.xph -> A.xE.xph)

Proof of Theorem hbe1

Step	Hyp	Ref	Expression
1		ax-ie1 1379	1 |- (E.xph -> A.xE.xph)

Syntax hints:   -> wi 4  A.wal 1240  E.wex 1378

This theorem was proved from axioms:  ax-ie1 1379

This theorem is referenced by:  nfe1  1382  19.8a  1479  exim  1487  19.43  1516  hbex  1524  excomim  1550  19.38  1563  exan  1580  equs5e  1673  exdistrfor  1678  hbmo1  1935  euan  1953  euor2  1955  eupicka  1977  mopick2  1980  moexexdc  1981  2moex  1983  2euex  1984  2exeu  1989  2eu4  1990  2eu7  1991