Theorem hbn 1003

Description: If x is not free in ph, it is not free in -. ph.

Hypothesis

Ref	Expression
hb.1	|- (ph -> A.xph)

Assertion

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

Proof of Theorem hbn

Step	Hyp	Ref	Expression
1		hbnt 1001	. 2 |- (A.x(ph -> A.xph) -> (-. ph -> A.x -. ph))
2		hb.1	. 2 |- (ph -> A.xph)
3	1, 2	mpg 985	1 |- (-. ph -> A.x -. ph)

Syntax hints:  -. wn 2   -> wi 3  A.wal 953

This theorem is referenced by:  hbex 1005  hbim 1006  hbor 1007  hban 1008  hbn1 1014  19.32 1085  19.41 1094  hbnae 1146  equsex 1151  a4ime 1159  cbvex 1165  sb8e 1261  dvelimALT 1352  mo 1392  euor 1397  2mo 1446  hbne 1642  cla4egf 1858  hbdif 2158  hbif 2370  caucvglem6 7115

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 962  ax-4 972  ax-5o 974  ax-6o 977

Copyright terms: Public domain