Theorem r19.23aivv 1287

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

Hypothesis

Ref	Expression
r19.23aivv.1	⊢ ((x ∈ A ∧ y ∈ B) → (φ → ψ))

Assertion

Ref	Expression
r19.23aivv	⊢ (∃x ∈ A ∃y ∈ B φ → ψ)

Distinct variable group(s):   x,y,ψ   y,A

Proof of Theorem r19.23aivv

Step	Hyp	Ref	Expression
1		r19.23aivv.1	. . . 4 ⊢ ((x ∈ A ∧ y ∈ B) → (φ → ψ))
2	1	exp 291	. . 3 ⊢ (x ∈ A → (y ∈ B → (φ → ψ)))
3	2	r19.23adv 1286	. 2 ⊢ (x ∈ A → (∃y ∈ B φ → ψ))
4	3	r19.23aiv 1284	1 ⊢ (∃x ∈ A ∃y ∈ B φ → ψ)

Syntax hints:   → wi 2   ∧ wa 196   ∈ wcel 1092  ∃wrex 1202

This theorem is referenced by:  tfrlem5 2953  xpdom2 3345  unfi 3441  kmlem8 3587  unxpdomlem 3649  qret 4631  qaddclt 4642  qnegclt 4643  qmulclt 4644  qrecclt 4646  xpnnen 4927  shscl 5282  shslej 5339  shsidm 5358  spansncv 5542  mdsymlem6 5781

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-17 925

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-rex 1206

metamath.org