Theorem hbn 1351

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

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

This theorem is referenced by:  hbex 1353  hbim 1354  hbor 1355  hban 1356  hbn1 1362  19.32 1438  19.41OLD 1449  hbnae 1507  equsex 1513  a4ime 1521  cbvex 1529  sb8e 1639  dvelimALT 1744  mo 1787  euor 1793  euor2 1839  2mo 1851  hbne 2103  hbnel 2104  cla4egf 2362  hbdif 2729  hbifOLD 3000  rexxpf 4044  ordtypelem6 5689  caucvglem6 8422  bnj1479 13155  bnj1390 13513  bnj1398 13515  bnj1443 13533  bnj1445 13535  bnj1449 13539  ordtypelem6OLD 15380  compab 16418

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321  ax-6o 1324

Copyright terms: Public domain