ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  hbe1 Unicode version

Theorem hbe1 1384
Description:  x is not free in  E. x ph. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
hbe1  |-  ( E. x ph  ->  A. x E. x ph )

Proof of Theorem hbe1
StepHypRef Expression
1 ax-ie1 1382 1  |-  ( E. x ph  ->  A. x E. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1241   E.wex 1381
This theorem was proved from axioms:  ax-ie1 1382
This theorem is referenced by:  nfe1  1385  19.8a  1482  exim  1490  19.43  1519  hbex  1527  excomim  1553  19.38  1566  exan  1583  equs5e  1676  exdistrfor  1681  hbmo1  1938  euan  1956  euor2  1958  eupicka  1980  mopick2  1983  moexexdc  1984  2moex  1986  2euex  1987  2exeu  1992  2eu4  1993  2eu7  1994
  Copyright terms: Public domain W3C validator