|   | 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 3168 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (∃𝑦 ∈ 𝐵 𝜓 → ∃𝑦 ∈ 𝐵 𝜒)) | 
| 4 | 3 | impr 454 | . 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝜓)) → ∃𝑦 ∈ 𝐵 𝜒) | 
| 5 | reximddv2.2 | . 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜓) | |
| 6 | 4, 5 | reximddv 3171 | 1 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝜒) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∧ wa 395 ∈ wcel 2108 ∃wrex 3070 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-rex 3071 | 
| This theorem is referenced by: r19.29vva 3216 r19.29vvaOLD 3217 prmgaplem8 17096 cpmadugsumfi 22883 cpmidg2sum 22886 cayhamlem4 22894 ltgseg 28604 cgraswap 28828 cgracom 28830 cgratr 28831 flatcgra 28832 dfcgra2 28838 xrofsup 32771 elrlocbasi 33270 aks6d1c2 42131 prmunb2 44330 | 
| Copyright terms: Public domain | W3C validator |