Theorem r19.23aivv 1794

Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version).

Hypothesis

Ref	Expression
r19.23aivv.1	|- ((x e. A /\ y e. B) -> (ph -> ps))

Assertion

Ref	Expression
r19.23aivv	|- (E.x e. A E.y e. B ph -> ps)

Distinct variable groups:   x,y,ps   y,A

Proof of Theorem r19.23aivv

Step	Hyp	Ref	Expression
1		r19.23aivv.1	. . 3 |- ((x e. A /\ y e. B) -> (ph -> ps))
2	1	r19.23adva 1793	. 2 |- (x e. A -> (E.y e. B ph -> ps))
3	2	r19.23aiv 1789	1 |- (E.x e. A E.y e. B ph -> ps)

Syntax hints:   -> wi 3   /\ wa 221   e. wcel 994  E.wrex 1692

This theorem is referenced by:  tfrlem5 4216  xpdom2 4583  unfi 4697  kmlem9 4919  unxpdomlem 4993  cnegex 5502  1re 5589  recex 5840  qre 6398  qaddcl 6408  qnegcl 6409  qmulcl 6410  qreccl 6412  cvganz 7127  xpnnen 7711  qdensere 7961  opnin 8079  blssioo 8124  tgioo 8126  xplm 8186  ipasslem5 8750  ipasslem11 8756  ubthlem14 8802  hhssnv 9410  shscli 9557  shsleji 9614  shsidmi 9633  spansncvi 9875  superpos 10562  irredi 10603  mdsymlem6 10617  ghomgrpilem2 10671  bsi2 11139  altretoplem2 11143  altretop 11144  lpni 11417  elfiun 11421  fbunfip 11631  hausfillim 11685  filnetlem1 11763  filnetlem4 11766  filnetlem5 11767  filnet 11768  haustlmu 11967  heiborlem29 12039

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

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-rex 1696

Copyright terms: Public domain