Theorem reximddv2 3225

Description: Double deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 15-Dec-2019.)

Hypotheses

Ref	Expression
reximddv2.1	⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒)
reximddv2.2	⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)

Assertion

Ref	Expression
reximddv2	⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)

Distinct variable groups:   𝑦,𝐴   𝜑,𝑥,𝑦

Allowed substitution hints:   𝜓(𝑥, 𝑦)   𝜒(𝑥, 𝑦)   𝐴(𝑥)   𝐵(𝑥, 𝑦)

Proof of Theorem reximddv2

Step	Hyp	Ref	Expression
1		reximddv2.1	. . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒)
2	1	ex 418	. . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒))
3	2	reximdva 3179	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐵 𝜓 → ∃𝑦 ∈ 𝐵 𝜒))
4	3	impr 460	. 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝜓)) → ∃𝑦 ∈ 𝐵 𝜒)
5		reximddv2.2	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓)
6	4, 5	reximddv 3182	1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3091

This theorem is used by:  r19.29vva  3226  prmgaplem8  17268  cpmadugsumfi  23228  cpmidg2sum  23231  cayhamlem4  23239  ltgseg  29092  cgraswap  29360  cgracom  29362  cgratr  29363  flatcgra  29365  dfcgra2  29371  xrofsup  33432  elrlocbasi  33904  zzedom  33939  aks6d1c2  43383  prmunb2  45498