Theorem hba1 1473

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

Syntax hints:   -> wi 4   A.wal 1282

This theorem was proved from axioms:  ax-ial 1467

This theorem is referenced by:  nfa1  1474  a5i  1475  hba2  1483  hbia1  1484  19.21h  1489  19.21ht  1513  exim  1530  19.12  1595  19.38  1606  ax9o  1628  equveli  1682  nfald  1683  equs5a  1715  ax11v2  1741  equs5  1750  equs5or  1751  sb56  1806  hbsb4t  1930  hbeu1  1951  eupickbi  2023  moexexdc  2025  2eu4  2034  exists2  2038  hbra1  2396