Theorem hbn 1004

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

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

This theorem is referenced by:  hbex 1006  hbim 1007  hbor 1008  hban 1009  hbn1 1015  19.32 1086  19.41 1095  hbnae 1147  equsex 1152  a4ime 1160  cbvex 1166  sb8e 1262  dvelimALT 1353  mo 1393  euor 1398  2mo 1447  hbne 1644  cla4egf 1861  hbdif 2161  hbif 2373  caucvglem6 7162

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-4 973  ax-5o 975  ax-6o 978

Copyright terms: Public domain