Theorem hbim 1043

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 1040	. . 3 |- (-. ph -> A.x -. ph)
3		pm2.21 76	. . 3 |- (-. ph -> (ph -> ps))
4	2, 3	19.21ai 1034	. 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 1034	. 2 |- (ps -> A.x(ph -> ps))
8	4, 7	ja 135	1 |- ((ph -> ps) -> A.x(ph -> ps))

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

This theorem is referenced by:  hbor 1044  hban 1045  hbbi 1046  hbia1 1050  19.21 1092  19.23 1099  19.38 1117  mo 1432  hbmo1 1445  hbmo 1446  moexex 1478  2mo 1487  2eu4 1492  2eu6 1494  hbral 1732  cbvralf 1842  vtocl2gf 1895  vtoclgaf 1897  rcla4 1917  moi 1971  dfss2f 2112  uniiunlem 2184  hbint 2610  elintab 2611  ssintab 2617  ssiun2s 2662  axrep2 2769  axrep3 2770  opelopabsb 2892  alxfr 3119  onminex 3164  tfis 3208  tfinds 3212  tfindes 3215  findes 3248  ralxp 3301  dmcosseq 3452  fneu 3698  fv3 3844  tz6.12c 3851  fvopab2 3902  dff13f 3989  tfr3 4227  dom2d 4545  ac6sfilem1 4588  ac6sfilem3 4590  aceq1 4875  aceq5lem5 4885  zfcndrep 5120  zfcndinf 5124  suppsrlem 5375  suppsr3 5378  uzindOLD 6379  nn0ind-raph 6385  uzind4s 6579  uzind4s2 6580  nnwof 6586  cau3ii 7117  caucvglem6 7365  cncnplem2 7985  iscaunns 8155  chcmhi 9389  atom1d 10561  tostos 10883  bwt2 11123  subtr 11395  subtr2 11396  ordtypelem5 11431  ordtypelem6 11432  ordtype 11434  omsubsdomlem2 11441  neibastop2lem1 11580  neibastop2lem3 11582  neibastop3 11585  limfilcf 11683  oprabopabf 11807  cncfres 11956

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-4 1009  ax-5o 1011  ax-6o 1014

Copyright terms: Public domain