Theorem hba1 1589

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

Step	Hyp	Ref	Expression
1		ax-ial 1583	1 |- ( A. x ph -> A. x A. x ph )

Syntax hints:   -> wi 4   A.wal 1396

This theorem was proved from axioms:  ax-ial 1583

This theorem is referenced by:  nfa1  1590  a5i  1592  hba2  1600  hbia1  1601  19.21h  1606  19.21ht  1630  exim  1648  19.12  1713  19.38  1724  ax9o  1746  equveli  1808  nfald  1809  equs5a  1843  ax11v2  1869  equs5  1878  equs5or  1879  sb56  1936  hbsb4t  2069  hbeu1  2092  eupickbi  2165  moexexdc  2167  2eu4  2176  exists2  2180  hbra1  2574