Theorem hba1 1520

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 1514	1 |- ( A. x ph -> A. x A. x ph )

Syntax hints:   -> wi 4   A.wal 1329

This theorem was proved from axioms:  ax-ial 1514

This theorem is referenced by:  nfa1  1521  a5i  1522  hba2  1530  hbia1  1531  19.21h  1536  19.21ht  1560  exim  1578  19.12  1643  19.38  1654  ax9o  1676  equveli  1732  nfald  1733  equs5a  1766  ax11v2  1792  equs5  1801  equs5or  1802  sb56  1857  hbsb4t  1988  hbeu1  2009  eupickbi  2081  moexexdc  2083  2eu4  2092  exists2  2096  hbra1  2465