Theorem hban 1045

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 1040	. . . 4 |- (-. ps -> A.x -. ps)
4	1, 3	hbim 1043	. . 3 |- ((ph -> -. ps) -> A.x(ph -> -. ps))
5	4	hbn 1040	. 2 |- (-. (ph -> -. ps) -> A.x -. (ph -> -. ps))
6		df-an 223	. 2 |- ((ph /\ ps) <-> -. (ph -> -. ps))
7	6	albii 1035	. 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 990

This theorem is referenced by:  hbbi 1046  hb3an 1048  19.21ad 1095  dvelimfALT 1190  equvini 1205  hbsb4 1286  sbcom 1296  cbval2 1354  cbvex2 1355  sb7f 1380  dvelimALT 1392  ax11indalem 1407  ax11inda2ALT 1408  a12lem1 1415  a12study 1417  a12studyALT 1418  mopick 1472  eupicka 1474  2eu6 1494  hbel 1609  clelab 1624  2ralbida 1723  hbrex 1734  hbrab 1819  cbvrexf 1843  cbvrex 1845  ceqsex2 1882  rcla4e 1918  eqvincf 1930  elrabf 1950  cbvrab 1956  moi 1971  reu2 1976  sbcralg 2044  sbcrexg 2045  csbnestglem 2087  csbnest1g 2089  hbdif 2213  hbin 2272  hbif 2427  hbuni 2575  eluniab 2579  cbvopab 2746  cbvopab1 2748  cbvopab1s 2749  axrep1 2768  axrep3 2770  axrep4 2771  axrep5 2772  opabid 2887  hbopab 2889  ralxfrd 3120  onminex 3164  peano5 3241  hbxp 3287  hbco 3377  hbcnv 3386  hbima 3503  hbfun 3641  imadif 3679  hbfn 3690  iunfopab 3719  hbf 3732  hbf1 3770  hbfo 3778  hbf1o 3795  fv3 3844  fvopab4gf 3892  hbiso 4006  isotrALT 4012  cbvoprab1 4057  cbvoprab12 4058  oprabval2gf 4086  oprabval4g 4091  oprabval4gALT 4092  dfoprab5sf 4178  elrnoprabg 4186  tfr3 4227  hbrdg 4237  tz7.49 4260  ac6sfilem3 4590  ac6sfi 4591  mapxpen 4642  xpmapenlem3 4645  xpmapenlem5 4647  nneneq 4659  hta 4874  ac6lem 4900  zorn2lem4 4937  zorn2lem5 4938  axextnd 5097  axrepndlem2 5099  axrepnd 5100  axunnd 5102  axpowndlem2 5104  axpowndlem4 5106  axpownd 5107  axregndlem2 5109  axregnd 5110  axinfndlem1 5111  axinfnd 5112  axacndlem4 5116  axacndlem5 5117  axacnd 5118  zfcndrep 5120  zfcndinf 5124  suppsr2 5377  suppsr3 5378  nnwof 6586  hbsum1 7186  hbsum 7187  clm4lei 7284  tgval3 7837  metequiv 8091  irred 10604  imgfldref2 10768  cmphmp 11027  homcard 11045  imonclem 11268  ismonc 11269  cmpmon 11270  iepiclem 11278  isepic 11279  finminlem 11418  inficlALT 11424  ordtypelem4 11430  ordtypelem7 11433  elomsubsd 11446  neibastop1 11579  neibastop2lem1 11580  neibastop2lem2 11581  neibastop2lem3 11582  neibastop2lem4 11583  neibastop3 11585  topmeet 11587  topjoin 11588  opabex3 11806  oprabopabf 11807  indexd 11846  indexf 11847  filbcmb 11857  sdclem2 11876  sdc 11877  fsumltisumi 11886  mettrifi 11912  totbndbnd 12000

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-4 1009  ax-5o 1011  ax-6o 1014

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

Copyright terms: Public domain