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

Theorem hbe1 1427
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 1425 1  |-  ( E. x ph  ->  A. x E. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1285   E.wex 1424
This theorem was proved from axioms:  ax-ie1 1425
This theorem is referenced by:  nfe1  1428  19.8a  1525  exim  1533  19.43  1562  hbex  1570  excomim  1596  19.38  1609  exan  1626  equs5e  1720  exdistrfor  1725  hbmo1  1983  euan  2001  euor2  2003  eupicka  2025  mopick2  2028  moexexdc  2029  2moex  2031  2euex  2032  2exeu  2037  2eu4  2038  2eu7  2039
  Copyright terms: Public domain W3C validator