Theorem hban 1356

Description: If x is not free in ph and ps, it is not free in (ph /\ ps).

Hypotheses

Ref	Expression
hb.1	|- (ph -> A.xph)
hb.2	|- (ps -> A.xps)

Assertion

Ref	Expression
hban	|- ((ph /\ ps) -> A.x(ph /\ ps))

Proof of Theorem hban

Step	Hyp	Ref	Expression
1		hb.1	. . . 4 |- (ph -> A.xph)
2		hb.2	. . . . 5 |- (ps -> A.xps)
3	2	hbn 1351	. . . 4 |- (-. ps -> A.x -. ps)
4	1, 3	hbim 1354	. . 3 |- ((ph -> -. ps) -> A.x(ph -> -. ps))
5	4	hbn 1351	. 2 |- (-. (ph -> -. ps) -> A.x -. (ph -> -. ps))
6		df-an 242	. 2 |- ((ph /\ ps) <-> -. (ph -> -. ps))
7	6	albii 1346	. 2 |- (A.x(ph /\ ps) <-> A.x -. (ph -> -. ps))
8	5, 6, 7	3imtr4i 236	1 |- ((ph /\ ps) -> A.x(ph /\ ps))

Syntax hints:  -. wn 2   -> wi 3   /\ wa 240  A.wal 1296

This theorem is referenced by:  hbbi 1357  hb3an 1359  19.21adOLD 1407  dvelimfALT 1514  equvini 1531  equviniOLD 1532  hbsb4 1620  sbcom 1632  cbval2 1698  cbvex2 1699  sb7fOLD 1732  dvelimALT 1744  ax11indalem 1759  ax11inda2ALT 1760  a12lem1 1767  a12study 1769  a12studyALT 1770  mopick 1833  eupicka 1835  mopick2 1837  2eu6 1858  hbel 1996  clelab 2013  2ralbida 2137  hbrex 2149  reean 2247  reeanOLD 2248  hbreu 2251  hbrab 2258  cbvrexf 2277  cbvreuv 2282  ceqsex2 2326  ceqsex2OLD 2327  rcla4e 2375  eqvincf 2389  elrabf 2413  cbvrab 2421  moi 2436  reu2 2442  sbcralgOLD 2532  sbcrexgOLD 2534  csbnestglem 2580  csbnest1g 2582  hbdif 2729  hbin 2800  hbif 2999  hbifOLD 3000  hbuni 3183  hbuniOLD 3184  eluniab 3189  cbvopab 3403  cbvopab1 3405  cbvopab1s 3406  axrep1 3429  axrep3 3431  axrep4 3432  axrep5 3433  opabidOLD 3558  hbopab 3560  hbopabOLD 3561  eufromeq4 3831  ralxfrd 3837  onminex 3888  peano5 3975  hbxp 4024  hbxpOLD 4025  hbco 4129  hbcnv 4139  hbimaOLD 4274  hbfun 4443  imadif 4493  hbfn 4509  iunfopabOLD 4543  hbf 4560  hbf1 4608  hbfo 4616  hbf1o 4633  fv3 4690  fvopab4gf 4744  hbiso 4868  hbisoOLD 4869  isotrALT 4875  cbvoprab1 4924  cbvoprab1OLD 4925  cbvoprab12 4926  cbvoprab12OLD 4927  oprabval2gf 4955  oprabval4g 4960  oprabval4gALT 4961  cbvmpt 5011  dfoprab5sf 5058  elrnoprabg 5066  hbiota1 5091  tfr3 5134  hbrdg 5144  tz7.49 5168  ac6sfilem3 5508  ac6sfi 5509  hbriota 5570  mapxpen 5589  xpmapenlem3 5592  xpmapenlem5 5594  nneneq 5606  ordtypelem4 5687  ordtypelem7 5690  hta 5858  elomsubsd 5885  ac6lem 5916  zorn2lem4 5953  zorn2lem5 5954  axextnd 6095  axrepndlem2 6097  axrepnd 6098  axunnd 6100  axpowndlem2 6102  axpowndlem4 6104  axpownd 6105  axregndlem2 6107  axregnd 6108  axinfndlem1 6109  axinfnd 6110  axacndlem4 6114  axacndlem5 6115  axacnd 6116  zfcndrep 6118  zfcndinf 6122  suppsr2 6375  suppsr3 6376  nnwof 7628  hbsum1 8243  hbsum 8244  clm4lei 8341  tgval3 8895  metequiv 9158  oprabopabf 10157  indexfi 10174  irred 11967  bnj912 12822  bnj921 12828  bnj919 12829  bnj982 12864  bnj1146 12943  bnj1306 13049  bnj1310 13050  bnj1351 13075  bnj1352 13076  bnj1347 13080  bnj1360 13085  bnj1379 13100  bnj1401 13113  bnj1441 13134  bnj1484 13159  bnj1492 13161  bnj594 13300  bnj849 13318  bnj964 13347  bnj1014 13374  bnj1123 13422  bnj1228 13456  bnj1309 13487  bnj1307 13488  bnj1321 13498  bnj1332 13499  bnj1398 13515  bnj1404 13517  bnj1417 13530  bnj1463 13550  bnj1491 13556  bnj1525 13572  axextdist 13866  axext4dist 13867  wfrlem4 13960  imgfldref2 14368  fopab2g 14485  hbcp 14500  npincppr 14501  iserzmulc1b 14528  dutos1 14626  hbprod1 14659  hbprod 14660  fnopabco2b 14734  curgrpact 14735  cmphmp 14878  homcard 14893  imonclem 15162  ismonc 15163  cmpmon 15164  iepiclem 15172  isepic 15173  finminlem 15367  inficlALT 15372  ordtypelem4OLD 15378  ordtypelem7OLD 15381  elomsubsdOLD 15394  neibastop1 15518  neibastop2lem1 15519  neibastop2lem2 15520  neibastop2lem3 15521  neibastop2lem4 15522  neibastop3 15524  topmeet 15526  topjoin 15527  morex 15662  opabex3 15701  cbvoprab2 15708  hbixp1 15725  indexdom 15754  indexfiOLD 15755  filbcmb 15776  sdclem2 15810  sdc 15811  fdc1 15813  fsumltisumi 15823  mettrifi 15847  cnopropabco 15917  cnoproprabco 15919  cnoprab1 15921  cnoprab2 15922  totbndbnd 15944  cbvrexcsf 16412  cbvreucsf 16413  cbvrabcsf 16414  elstrdiff 16720  stb2xpl 16742  glbconx 17029  pmapglb2x 17254

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

This theorem depends on definitions:  df-bi 164  df-an 242

Copyright terms: Public domain