Theorem r19.23aivv 1751

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

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

This theorem is referenced by:  tfrlem5 3921  xpdom2 4448  unfi 4563  unfiOLD 4564  kmlem9 4783  unxpdomlem 4854  cnegext 5360  1re 5447  recext 5696  qret 6260  qaddclt 6270  qnegclt 6271  qmulclt 6272  qrecclt 6274  cvganz 6924  xpnnen 7500  qdensere 7748  opnin 7866  blssioo 7910  tgioo 7912  xplm 7972  ipasslem5 8490  ipasslem11 8496  ubthlem14 8538  hhssnv 9129  shscl 9276  shslej 9333  shsidm 9352  spansncv 9592  superpos 10276  irred 10316  mdsymlem6 10330  ghomgrpilem2 10381

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-rex 1653

Copyright terms: Public domain