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

Theorem hba1 1476
Description: 𝑥 is not free in 𝑥𝜑. 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 (∀𝑥𝜑 → ∀𝑥𝑥𝜑)

Proof of Theorem hba1
StepHypRef Expression
1 ax-ial 1470 1 (∀𝑥𝜑 → ∀𝑥𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1285
This theorem was proved from axioms:  ax-ial 1470
This theorem is referenced by:  nfa1  1477  a5i  1478  hba2  1486  hbia1  1487  19.21h  1492  19.21ht  1516  exim  1533  19.12  1598  19.38  1609  ax9o  1631  equveli  1686  nfald  1687  equs5a  1719  ax11v2  1745  equs5  1754  equs5or  1755  sb56  1810  hbsb4t  1934  hbeu1  1955  eupickbi  2027  moexexdc  2029  2eu4  2038  exists2  2042  hbra1  2404
  Copyright terms: Public domain W3C validator