Theorem hbim 1005

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 1002	. . 3 |- (-. ph -> A.x -. ph)
3		pm2.21 76	. . 3 |- (-. ph -> (ph -> ps))
4	2, 3	19.21ai 996	. 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 996	. 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 952

This theorem is referenced by:  hbor 1006  hban 1007  hbbi 1008  hbia1 1012  19.21 1054  19.23 1061  19.38 1079  mo 1391  hbmo1 1404  hbmo 1405  moexex 1436  2mo 1445  2eu4 1450  2eu6 1452  hbral 1683  cbvralf 1793  vtocl2gf 1845  vtoclgaf 1847  rcla4 1867  moi 1921  dfss2f 2056  uniiunlem 2128  hbint 2538  elintab 2539  ssintab 2545  ssiun2s 2589  axrep2 2690  axrep3 2691  opabsb 2810  alxfr 2891  onminex 3015  tfis 3122  findes 3155  tfinds 3156  tfindes 3159  ralxp 3213  dmcosseq 3357  fneu 3584  fv3 3724  tz6.12c 3731  fvopab2 3782  f1fvf 3866  tfr3 3917  dom2d 4391  aceq1 4709  aceq5lem5 4719  zfcndrep 4946  zfcndinf 4950  suppsrlem 5201  suppsr3 5204  uzindOLD 6164  nn0ind-raph 6170  uzind4s 6392  uzind4s2 6393  nnwof 6399  cau3i 6859  caucvglem6 7106  cncnplem2 7725  chcmh 9052  atom1d 10217

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-4 971  ax-5o 973  ax-6o 976

Copyright terms: Public domain