Theorem hbim 1004

Description: If x is not free in ph and ps, it is not free in (ph -> ps). (The proof was shortened by O'Cat, 3-Mar-2008.)

Hypotheses

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

Assertion

Ref	Expression
hbim	|- ((ph -> ps) -> A.x(ph -> ps))

Proof of Theorem hbim

Step	Hyp	Ref	Expression
1		hb.1	. . . 4 |- (ph -> A.xph)
2	1	hbn 1001	. . 3 |- (-. ph -> A.x -. ph)
3		pm2.21 76	. . 3 |- (-. ph -> (ph -> ps))
4	2, 3	19.21ai 995	. 2 |- (-. ph -> A.x(ph -> ps))
5		hb.2	. . 3 |- (ps -> A.xps)
6		ax-1 4	. . 3 |- (ps -> (ph -> ps))
7	5, 6	19.21ai 995	. 2 |- (ps -> A.x(ph -> ps))
8	4, 7	ja 137	1 |- ((ph -> ps) -> A.x(ph -> ps))

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

This theorem is referenced by:  hbor 1005  hban 1006  hbbi 1007  19.21 1052  19.23 1059  19.38 1077  mo 1386  hbmo1 1399  hbmo 1400  moexex 1431  2mo 1440  2eu4 1445  2eu6 1447  hbral 1678  cbvralf 1788  vtocl2gf 1840  vtoclgaf 1842  rcla4 1862  moi 1915  dfss2f 2050  uniiunlem 2122  hbint 2533  elintab 2534  ssintab 2540  ssiun2s 2584  axrep2 2685  axrep3 2686  opabsb 2804  alxfr 2886  onminex 3010  tfis 3117  findes 3150  tfinds 3151  tfindes 3154  ralxp 3208  dmcosseq 3349  fneu 3578  fv3 3718  tz6.12c 3725  fvopab2 3776  f1fvf 3860  tfr3 3911  dom2d 4385  aceq1 4701  aceq5lem5 4711  zfcndrep 4938  zfcndinf 4942  suppsrlem 5193  suppsr3 5196  uzindOLD 6156  nn0ind-raph 6162  uzind4s 6384  uzind4s2 6385  nnwof 6391  cau3i 6851  caucvglem6 7098  cncnplem2 7714  chcmh 9034  atom1d 10188

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