Theorem hbim 1354

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 1351	. . 3 |- (-. ph -> A.x -. ph)
3		pm2.21 92	. . 3 |- (-. ph -> (ph -> ps))
4	2, 3	19.21ai 1345	. 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 1345	. 2 |- (ps -> A.x(ph -> ps))
8	4, 7	ja 152	1 |- ((ph -> ps) -> A.x(ph -> ps))

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

This theorem is referenced by:  hbor 1355  hban 1356  hbbi 1357  hbia1 1361  19.21 1403  19.23 1411  19.38 1432  mo 1787  hbmo1 1802  hbmo 1803  moexex 1841  2mo 1851  2eu4 1856  2eu6 1858  hbral 2146  cbvralf 2276  vtocl2gf 2348  vtoclgaf 2350  vtoclgafOLD 2351  rcla4 2373  rcla4OLD 2374  moi 2436  dfss2f 2612  uniiunlem 2693  hbif 2999  hbintOLD 3226  elintab 3227  ssintab 3233  ssintabOLD 3234  ssiun2s 3297  axrep2 3430  axrep3 3431  opelopabsbOLD 3565  eufromeq4 3831  alxfr 3836  onminex 3888  tfis 3938  tfinds 3942  tfindsOLD 3943  tfindes 3946  findes 3983  ralxp 4041  dmcosseqOLD 4215  fneuOLD 4518  fv3 4690  tz6.12c 4697  fvopab2 4754  dff13f 4851  tfr3 5134  dom2d 5463  ac6sfilem1 5506  ac6sfilem3 5508  ordtypelem5 5688  ordtypelem6 5689  ordtype 5691  omsubsdomlem2 5880  aceq1 5891  aceq5lem5 5901  zfcndrep 6118  zfcndinf 6122  suppsrlem 6373  suppsr3 6376  uzindOLD 7420  nn0ind-raph 7426  uzind4s 7621  uzind4s2 7622  nnwof 7628  cau3ii 8166  caucvglem6 8422  cncnplem2 9052  iscaunns 9222  oprabopabf 10157  chcmhi 10746  atom1d 11925  bnj47 12417  bnj48 12422  bnj1306 13049  bnj1310 13050  bnj1385 13102  bnj1468 13145  bnj1492 13161  bnj900 13325  bnj981 13356  bnj1014 13374  bnj1123 13422  bnj1129 13425  bnj1128 13428  bnj1137 13433  bnj1332 13499  bnj1375 13509  bnj1376 13510  bnj1497 13560  r19.21 13818  setinds 13844  tfisg 13912  wfisg 13917  frinsg 13941  tostos 14637  fprodneg 14741  bwt2 14960  cntrsetlem 14999  subtr 15352  subtr2 15353  ordtypelem5OLD 15379  ordtypelem6OLD 15380  ordtypeOLD 15382  omsubsdomlem2OLD 15389  neibastop2lem1 15519  neibastop2lem3 15521  neibastop3 15524  limfilcf 15587  findcard2 15745  fdc1 15813  oprpiece1res2 15881  cncfres 15895  cnresoprab 15915  pm11.71 16354  rcla4t 16407  cbvralcsf 16411

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321  ax-6o 1324

Copyright terms: Public domain