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 4404  aceq1 4729  aceq5lem5 4739  zfcndrep 4966  zfcndinf 4970  suppsrlem 5221  suppsr3 5224  uzindOLD 6208  nn0ind-raph 6214  uzind4s 6452  uzind4s2 6453  nnwof 6459  cau3i 6914  caucvglem6 7162  cncnplem2 7775  iscaunns 7944  chcmh 9113  atom1d 10280

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