Theorem 2r19.29 16243

Description: Double the quantifiers of theorem r19.29.

Assertion

Ref	Expression
2r19.29	|- ((A.x e. A A.y e. B ph /\ E.x e. A E.y e. B ps) -> E.x e. A E.y e. B (ph /\ ps))

Proof of Theorem 2r19.29

Step	Hyp	Ref	Expression
1		r19.29 2227	. 2 |- ((A.x e. A A.y e. B ph /\ E.x e. A E.y e. B ps) -> E.x e. A (A.y e. B ph /\ E.y e. B ps))
2		r19.29 2227	. . 3 |- ((A.y e. B ph /\ E.y e. B ps) -> E.y e. B (ph /\ ps))
3	2	reximi 2198	. 2 |- (E.x e. A (A.y e. B ph /\ E.y e. B ps) -> E.x e. A E.y e. B (ph /\ ps))
4	1, 3	syl 12	1 |- ((A.x e. A A.y e. B ph /\ E.x e. A E.y e. B ps) -> E.x e. A E.y e. B (ph /\ ps))

Syntax hints:   -> wi 3   /\ wa 240  A.wral 2105  E.wrex 2106

This theorem is referenced by:  prter2 16285

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

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

Copyright terms: Public domain