Theorem r19.23aivv 1740

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

Syntax hints:   -> wi 3   /\ wa 223   e. wcel 955  E.wrex 1638

This theorem is referenced by:  tfrlem5 3900  xpdom2 4422  unfi 4528  kmlem9 4745  unxpdomlem 4815  cnegext 5320  1re 5407  recext 5657  qret 6197  qaddclt 6207  qnegclt 6208  qmulclt 6209  qrecclt 6211  cvganz 6861  xpnnen 7441  qdensere 7691  opnin 7809  blssioo 7852  tgioo 7854  xplm 7909  ipasslem5 8425  ipasslem11 8431  ubthlem14 8473  hhssnv 9054  shscl 9196  shslej 9253  shsidm 9272  spansncv 9514  superpos 10189  irred 10229  mdsymlem6 10243  ghomgrpilem2 10291

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-rex 1642

Copyright terms: Public domain