Theorem hban 1011

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 1006	. . . 4 |- (-. ps -> A.x -. ps)
4	1, 3	hbim 1009	. . 3 |- ((ph -> -. ps) -> A.x(ph -> -. ps))
5	4	hbn 1006	. 2 |- (-. (ph -> -. ps) -> A.x -. (ph -> -. ps))
6		df-an 225	. 2 |- ((ph /\ ps) <-> -. (ph -> -. ps))
7	6	albii 1001	. 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 956

This theorem is referenced by:  hbbi 1012  hb3an 1014  19.21ad 1061  dvelimfALT 1155  equvini 1170  hbsb4 1250  sbcom 1260  cbval2 1318  cbvex2 1319  sb7f 1343  dvelimALT 1355  ax11indalem 1370  ax11inda2ALT 1371  a12lem1 1378  a12study 1380  a12studyALT 1381  mopick 1435  eupicka 1437  2eu6 1457  hbel 1569  clelab 1584  2ralbida 1680  hbrex 1691  hbrab 1776  cbvrexf 1800  cbvrex 1802  ceqsex2 1839  rcla4e 1875  eqvincf 1887  elrabf 1907  cbvrab 1913  moi 1928  reu2 1933  sbcralg 1997  sbcrexg 1998  csbnestglem 2038  csbnest1g 2040  hbdif 2164  hbin 2223  hbif 2377  hbuni 2513  eluniab 2517  cbvopab 2677  cbvopab1 2679  cbvopab1s 2680  axrep1 2699  axrep3 2701  axrep4 2702  axrep5 2703  opabid 2816  hbopab 2818  ralxfrd 2903  onminex 3026  peano5 3159  hbxp 3210  hbco 3293  hbcnv 3301  hbima 3417  hbfun 3542  imadif 3580  hbfn 3590  hbf 3631  hbf1 3669  hbfo 3677  hbf1o 3693  fv3 3739  fvopab4gf 3787  hbiso 3898  isotrALT 3904  tfr3 3932  hbrdg 3942  tz7.49 3965  cbvoprab12 4004  oprabval2gf 4032  oprabval4g 4037  elrnoprabg 4130  mapxpen 4501  xpmapenlem3 4504  xpmapenlem5 4506  nneneq 4518  hta 4738  ac6lem 4764  zorn2lem4 4801  zorn2lem5 4802  axextnd 4955  axrepndlem2 4957  axrepnd 4958  axunnd 4960  axpowndlem2 4962  axpowndlem4 4964  axpownd 4965  axregndlem2 4967  axregnd 4968  axinfndlem1 4969  axinfnd 4970  axacndlem4 4974  axacndlem5 4975  axacnd 4976  zfcndrep 4978  zfcndinf 4982  suppsr2 5235  suppsr3 5236  nnwof 6460  hbsum1 6983  hbsum 6984  clm4le 7081  tgval3t 7624  irredt 10317  cmphmp 10507  homcard 10525  imonclem 10712  ismonc 10713  cmpmon 10714

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-4 975  ax-5o 977  ax-6o 980

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

Copyright terms: Public domain