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

Theorem hba1 1415
Description: x is not free in xφ. Example in Appendix in [Megill] p. 450 (p. 19 of the preprint). Also Lemma 22 of [Monk2] p. 114. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
hba1 (xφxxφ)

Proof of Theorem hba1
StepHypRef Expression
1 ax-ial 1409 1 (xφxxφ)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1226
This theorem was proved from axioms:  ax-ial 1409
This theorem is referenced by:  nfa1  1416  a5i  1417  hba2  1425  hbia1  1426  19.21h  1431  19.21ht  1455  exim  1472  19.12  1537  19.38  1548  ax9o  1570  equveli  1624  nfald  1625  equs5a  1657  ax11v2  1683  equs5  1692  equs5or  1693  sb56  1747  hbsb4t  1871  hbeu1  1892  eupickbi  1964  moexexdc  1966  2eu4  1975  exists2  1979  hbra1  2332
  Copyright terms: Public domain W3C validator