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

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

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