Theorem r19.23advv 1746

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 1743	. 2 |- ((ph /\ x e. A) -> (E.y e. B ps -> ch))
5	4	r19.23adva 1744	1 |- (ph -> (E.x e. A E.y e. B ps -> ch))

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

This theorem is referenced by:  xpdom2 4428  rankxplim3 4694  brdom6disj 4785  unxpdomlem 4823  qaddclt 6215  qmulclt 6217  climaddlem3 7060  climmullem8 7071  xpnnen 7449  infxpidmlem7 7509  rnblssm 7803  blss 7805  opnin 7821  xpcn 7926  bcthlem33 7981  shselt 9216  shmods 9300  sumdmdlem 10281  cdjreu 10293  cdj3lem2a 10297  cdj3lem2b 10298  cdj3lem3a 10300  cdj3 10302

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-rex 1647

Copyright terms: Public domain