Theorem hban 1006

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 1001	. . . 4 |- (-. ps -> A.x -. ps)
4	1, 3	hbim 1004	. . 3 |- ((ph -> -. ps) -> A.x(ph -> -. ps))
5	4	hbn 1001	. 2 |- (-. (ph -> -. ps) -> A.x -. (ph -> -. ps))
6		df-an 225	. 2 |- ((ph /\ ps) <-> -. (ph -> -. ps))
7	6	albii 996	. 2 |- (A.x(ph /\ ps) <-> A.x -. (ph -> -. ps))
8	5, 6, 7	3imtr4 219	1 |- ((ph /\ ps) -> A.x(ph /\ ps))

Syntax hints:  -. wn 2   -> wi 3   /\ wa 223  A.wal 951

This theorem is referenced by:  hbbi 1007  hb3an 1009  19.21ad 1055  dvelimfALT 1149  equvini 1164  hbsb4 1243  sbcom 1253  cbval2 1311  cbvex2 1312  sb7f 1336  ax11indalem 1361  ax11inda2ALT 1362  a12lem1 1369  a12study 1371  a12studyALT 1372  mopick 1426  2eu6 1447  hbel 1558  clelab 1573  2ralbida 1669  hbrex 1680  hbrab 1765  cbvrex 1790  ceqsex2 1827  rcla4e 1863  eqvincf 1875  elrabf 1895  cbvrab 1901  moi 1915  reu2 1920  sbcralg 1984  sbcrexg 1985  csbnestglem 2025  csbnest1g 2027  hbdif 2151  hbin 2210  hbif 2363  hbuni 2499  eluniab 2503  cbvopab 2662  cbvopab1 2664  cbvopab1s 2665  axrep1 2684  axrep3 2686  axrep4 2687  axrep5 2688  opabid 2799  hbopab 2801  ralxfrd 2887  onminex 3010  peano5 3143  hbxp 3194  hbco 3276  hbcnv 3284  hbima 3395  hbfun 3522  imadif 3560  hbfn 3570  hbf 3611  hbf1 3648  hbfo 3656  hbf1o 3672  fv3 3718  fvopab4gf 3766  hbiso 3877  isotrALT 3883  tfr3 3911  hbrdg 3921  tz7.49 3944  cbvoprab12 3983  oprabval2gf 4011  oprabval4g 4016  elrnoprabg 4108  mapxpen 4475  xpmapenlem3 4478  xpmapenlem5 4480  nneneq 4492  hta 4700  ac6lem 4726  zorn2lem4 4763  zorn2lem5 4764  axextnd 4915  axrepndlem2 4917  axrepnd 4918  axunnd 4920  axpowndlem2 4922  axpowndlem4 4924  axpownd 4925  axregndlem2 4927  axregnd 4928  axinfndlem1 4929  axinfnd 4930  axacndlem4 4934  axacndlem5 4935  axacnd 4936  zfcndrep 4938  zfcndinf 4942  suppsr2 5195  suppsr3 5196  nnwof 6391  hbsum1 6921  hbsum 6922  clm4le 7019  tgval3t 7567  irredt 10230  cbvrexf 10338  cmphmp 10408  homcard 10426  imonclem 10583  ismonc 10584  cmpmon 10585

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-4 970  ax-5o 972  ax-6o 975

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain