Theorem hbim 1007

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

This theorem is referenced by:  hbor 1008  hban 1009  hbbi 1010  hbia1 1014  19.21 1056  19.23 1063  19.38 1081  mo 1393  hbmo1 1406  hbmo 1407  moexex 1438  2mo 1447  2eu4 1452  2eu6 1454  hbral 1686  cbvralf 1796  vtocl2gf 1849  vtoclgaf 1851  rcla4 1871  moi 1925  dfss2f 2060  uniiunlem 2132  hbint 2543  elintab 2544  ssintab 2550  ssiun2s 2594  axrep2 2695  axrep3 2696  opabsb 2815  alxfr 2896  onminex 3020  tfis 3127  findes 3160  tfinds 3161  tfindes 3164  ralxp 3218  dmcosseq 3365  fneu 3592  fv3 3733  tz6.12c 3740  fvopab2 3791  f1fvf 3875  tfr3 3926  dom2d 4403  aceq1 4721  aceq5lem5 4731  zfcndrep 4958  zfcndinf 4962  suppsrlem 5213  suppsr3 5216  uzindOLD 6196  nn0ind-raph 6202  uzind4s 6438  uzind4s2 6439  nnwof 6445  cau3i 6899  caucvglem6 7147  cncnplem2 7760  iscaunns 7929  chcmh 9098  atom1d 10265

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