Theorem hbn 1001

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 999	. 2 |- (A.x(ph -> A.xph) -> (-. ph -> A.x -. ph))
2		hb.1	. 2 |- (ph -> A.xph)
3	1, 2	mpg 983	1 |- (-. ph -> A.x -. ph)

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

This theorem is referenced by:  hbex 1003  hbim 1004  hbor 1005  hban 1006  hbn1 1011  19.32 1082  19.41 1091  hbnae 1143  equsex 1148  a4ime 1156  cbvex 1162  sb8e 1257  mo 1386  euor 1391  2mo 1440  hbne 1636  cla4egf 1852  hbdif 2151  hbif 2363  caucvglem6 7098

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-4 970  ax-5o 972  ax-6o 975

Copyright terms: Public domain