Theorem hbn1 1741

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

Assertion

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

Proof of Theorem hbn1

Step	Hyp	Ref	Expression
1		ax-6 1740	1 |- ( -. A. x ph -> A. x -. A. x ph )

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

This theorem is referenced by:  hbe1  1742  modal-5  1744  ax5o  1761  hbnOLD  1798  hba1OLD  1801  hbimdOLD  1831  dvelimhwOLD  1873  ax12olem6OLD  1982  dvelimvOLD  1994  a16gOLD  2013  ax15  2070  dvelimALT  2183  ax11indn  2245  vk15.4j  28323  a9e2nd  28356  a9e2ndVD  28729  a9e2ndALT  28752  dvelimhwNEW7  29161  ax12olem6NEW7  29165  dvelimvNEW7  29168  dvelimhvAUX7  29198  equs5NEW7  29238  ax15NEW7  29240  a16gNEW7  29250  dvelimALTNEW7  29337

This theorem was proved from axioms:  ax-6 1740