Theorem hbn1 1730

Description: x is not free in -. A.xph. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 18-Aug-2014.)

Assertion

Ref	Expression
hbn1	|- (-. A.xph -> A.x -. A.xph)

Proof of Theorem hbn1

Step	Hyp	Ref	Expression
1		ax-6 1729	1 |- (-. A.xph -> A.x -. A.xph)

Syntax hints:  -. wn 3   -> wi 4  A.wal 1540

This theorem was proved from axioms:  ax-6 1729

This theorem is referenced by:  hbe1  1731  modal-5  1733  ax5o  1749  hbnOLD  1777  hba1OLD  1787  hbimdOLD  1816  dvelimhw  1849  ax12olem6  1932  dvelimv  1939  a16g  1945  ax15  2021  dvelimALT  2133  ax11indn  2195