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

Theorem hbe1 1381
Description: x is not free in xφ. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
hbe1 (xφxxφ)

Proof of Theorem hbe1
StepHypRef Expression
1 ax-ie1 1379 1 (xφxxφ)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1240  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
  Copyright terms: Public domain W3C validator