Theorem hban 1041

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 1036	. . . 4 |- (-. ps -> A.x -. ps)
4	1, 3	hbim 1039	. . 3 |- ((ph -> -. ps) -> A.x(ph -> -. ps))
5	4	hbn 1036	. 2 |- (-. (ph -> -. ps) -> A.x -. (ph -> -. ps))
6		df-an 223	. 2 |- ((ph /\ ps) <-> -. (ph -> -. ps))
7	6	albii 1031	. 2 |- (A.x(ph /\ ps) <-> A.x -. (ph -> -. ps))
8	5, 6, 7	3imtr4i 217	1 |- ((ph /\ ps) -> A.x(ph /\ ps))

Syntax hints:  -. wn 2   -> wi 3   /\ wa 221  A.wal 986

This theorem is referenced by:  hbbi 1042  hb3an 1044  19.21ad 1091  dvelimfALT 1186  equvini 1201  hbsb4 1281  sbcom 1291  cbval2 1349  cbvex2 1350  sb7f 1374  dvelimALT 1386  ax11indalem 1401  ax11inda2ALT 1402  a12lem1 1409  a12study 1411  a12studyALT 1412  mopick 1466  eupicka 1468  2eu6 1488  hbel 1603  clelab 1618  2ralbida 1715  hbrex 1726  hbrab 1811  cbvrexf 1835  cbvrex 1837  ceqsex2 1874  rcla4e 1910  eqvincf 1922  elrabf 1942  cbvrab 1948  moi 1963  reu2 1968  sbcralg 2036  sbcrexg 2037  csbnestglem 2079  csbnest1g 2081  hbdif 2205  hbin 2264  hbif 2418  hbuni 2557  eluniab 2561  cbvopab 2723  cbvopab1 2725  cbvopab1s 2726  axrep1 2745  axrep3 2747  axrep4 2748  axrep5 2749  opabid 2863  hbopab 2865  ralxfrd 2952  onminex 3075  peano5 3215  hbxp 3261  hbco 3350  hbcnv 3359  hbima 3474  hbfun 3611  imadif 3649  hbfn 3659  hbf 3700  hbf1 3738  hbfo 3746  hbf1o 3763  fv3 3809  fvopab4gf 3857  hbiso 3968  isotrALT 3974  tfr3 4002  hbrdg 4012  tz7.49 4035  cbvoprab1 4074  cbvoprab12 4075  oprabval2gf 4103  oprabval4g 4108  oprabval4gALT 4109  elrnoprabg 4204  mapxpen 4584  xpmapenlem3 4587  xpmapenlem5 4589  nneneq 4601  hta 4814  ac6lem 4840  zorn2lem4 4877  zorn2lem5 4878  axextnd 5032  axrepndlem2 5034  axrepnd 5035  axunnd 5037  axpowndlem2 5039  axpowndlem4 5041  axpownd 5042  axregndlem2 5044  axregnd 5045  axinfndlem1 5046  axinfnd 5047  axacndlem4 5051  axacndlem5 5052  axacnd 5053  zfcndrep 5055  zfcndinf 5059  suppsr2 5312  suppsr3 5313  nnwof 6519  hbsum1 7106  hbsum 7107  clm4lei 7204  tgval3 7749  irred 10440  cmphmp 10657  homcard 10675  imonclem 10876  ismonc 10877  cmpmon 10878  iepiclem 10886  isepic 10887

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 995  ax-4 1005  ax-5o 1007  ax-6o 1010

This theorem depends on definitions:  df-bi 145  df-an 223

Copyright terms: Public domain