Theorem r19.23advv 1749

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

Hypothesis

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

Assertion

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

Distinct variable groups:   x,y,ph   ch,x,y   y,A

Proof of Theorem r19.23advv

Step	Hyp	Ref	Expression
1		r19.23advv.1	. . . . 5 |- (ph -> ((x e. A /\ y e. B) -> (ps -> ch)))
2	1	exp3a 375	. . . 4 |- (ph -> (x e. A -> (y e. B -> (ps -> ch))))
3	2	imp 350	. . 3 |- ((ph /\ x e. A) -> (y e. B -> (ps -> ch)))
4	3	r19.23adv 1746	. 2 |- ((ph /\ x e. A) -> (E.y e. B ps -> ch))
5	4	r19.23adva 1747	1 |- (ph -> (E.x e. A E.y e. B ps -> ch))

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

This theorem is referenced by:  xpdom2 4442  rankxplim3 4714  brdom6disj 4805  unxpdomlem 4843  qaddclt 6269  qmulclt 6271  climaddlem3 7116  climmullem8 7127  xpnnen 7499  infxpidmlem7 7558  rnblssm 7851  blss 7853  opnin 7869  xpcn 7976  bcthlem33 8031  shselt 9278  shmods 9362  sumdmdlem 10345  cdjreu 10359  cdj3lem2a 10363  cdj3lem2b 10364  cdj3lem3a 10366  cdj3 10368

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-rex 1650

Copyright terms: Public domain