![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > reximddv2 | Structured version Visualization version GIF version |
Description: Double deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Thierry Arnoux, 15-Dec-2019.) |
Ref | Expression |
---|---|
reximddv2.1 | ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒) |
reximddv2.2 | ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) |
Ref | Expression |
---|---|
reximddv2 | ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reximddv2.1 | . . . . 5 ⊢ ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) ∧ 𝜓) → 𝜒) | |
2 | 1 | ex 412 | . . . 4 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → (𝜓 → 𝜒)) |
3 | 2 | reximdva 3165 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐵 𝜓 → ∃𝑦 ∈ 𝐵 𝜒)) |
4 | 3 | impr 454 | . 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝜓)) → ∃𝑦 ∈ 𝐵 𝜒) |
5 | reximddv2.2 | . 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) | |
6 | 4, 5 | reximddv 3168 | 1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2105 ∃wrex 3067 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1776 df-rex 3068 |
This theorem is referenced by: r19.29vva 3213 r19.29vvaOLD 3214 prmgaplem8 17091 cpmadugsumfi 22898 cpmidg2sum 22901 cayhamlem4 22909 ltgseg 28618 cgraswap 28842 cgracom 28844 cgratr 28845 flatcgra 28846 dfcgra2 28852 xrofsup 32777 elrlocbasi 33252 aks6d1c2 42111 prmunb2 44306 |
Copyright terms: Public domain | W3C validator |