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

Theorem hba1 1474
Description:  x is not free in  A. x ph. 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  |-  ( A. x ph  ->  A. x A. x ph )

Proof of Theorem hba1
StepHypRef Expression
1 ax-ial 1468 1  |-  ( A. x ph  ->  A. x A. x ph )
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1283
This theorem was proved from axioms:  ax-ial 1468
This theorem is referenced by:  nfa1  1475  a5i  1476  hba2  1484  hbia1  1485  19.21h  1490  19.21ht  1514  exim  1531  19.12  1596  19.38  1607  ax9o  1629  equveli  1683  nfald  1684  equs5a  1716  ax11v2  1742  equs5  1751  equs5or  1752  sb56  1807  hbsb4t  1931  hbeu1  1952  eupickbi  2024  moexexdc  2026  2eu4  2035  exists2  2039  hbra1  2397
  Copyright terms: Public domain W3C validator