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

Theorem hba1 1505
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 1499 1 (∀𝑥𝜑 → ∀𝑥𝑥𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1314
This theorem was proved from axioms:  ax-ial 1499
This theorem is referenced by:  nfa1  1506  a5i  1507  hba2  1515  hbia1  1516  19.21h  1521  19.21ht  1545  exim  1563  19.12  1628  19.38  1639  ax9o  1661  equveli  1717  nfald  1718  equs5a  1750  ax11v2  1776  equs5  1785  equs5or  1786  sb56  1841  hbsb4t  1966  hbeu1  1987  eupickbi  2059  moexexdc  2061  2eu4  2070  exists2  2074  hbra1  2442
  Copyright terms: Public domain W3C validator