Theorem r19.23aivv 2217

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 2216	. 2 |- (x e. A -> (E.y e. B ph -> ps))
3	2	r19.23aiv 2211	1 |- (E.x e. A E.y e. B ph -> ps)

Syntax hints:   -> wi 3   /\ wa 240   e. wcel 1300  E.wrex 2106

This theorem is referenced by:  tfrlem5 5123  xpdom2 5501  unfi 5644  kmlem9 5935  unxpdomlem 5995  cnegex 6502  1re 6598  recex 6876  qre 7439  qaddcl 7449  qnegcl 7450  qmulcl 7451  qreccl 7453  cvganz 8176  xpnnen 8768  qdensere 9027  opnin 9146  blssioo 9191  tgioo 9193  xplm 9253  ipasslem5 9835  ipasslem11 9841  ubthlem14 9887  fbunfip 10282  hausfillim 10303  lpni 10347  hhssnv 10767  shscli 10914  shsleji 10971  shsidmi 10990  spansncvi 11232  superpos 11926  irredi 11966  mdsymlem6 11980  ghomgrpilem2 13629  eucalginv 13752  eucalglt 13753  poseq 13954  soseq 13955  axfelem15 14045  elaltxp 14098  altopelaltxp 14099  altxpsspw 14100  repcpwti 14503  bsi2 14992  altretoplem2 14996  altretop 14997  elfiun 15369  filnetlem1 15640  filnetlem4 15643  filnetlem5 15644  filnet 15645  haustlmu 15906  txmet 15925  heiborlem29 15983  isline 17220

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-ral 2109  df-rex 2110

Copyright terms: Public domain